Mathbox for Norm Megill < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  diblss Unicode version

Theorem diblss 31653
 Description: The value of partial isomorphism B is a subspace of partial vector space H. TODO: use dib* specific theorems instead of dia* ones to shorten proof? (Contributed by NM, 11-Feb-2014.)
Hypotheses
Ref Expression
diblss.b
diblss.l
diblss.h
diblss.u
diblss.i
diblss.s
Assertion
Ref Expression
diblss

Proof of Theorem diblss
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqidd 2405 . 2 Scalar Scalar
2 diblss.h . . . . 5
3 eqid 2404 . . . . 5
4 diblss.u . . . . 5
5 eqid 2404 . . . . 5 Scalar Scalar
6 eqid 2404 . . . . 5 Scalar Scalar
72, 3, 4, 5, 6dvhbase 31566 . . . 4 Scalar
87eqcomd 2409 . . 3 Scalar
10 eqid 2404 . . . . 5
11 eqid 2404 . . . . 5
122, 10, 3, 4, 11dvhvbase 31570 . . . 4
1312eqcomd 2409 . . 3
15 eqidd 2405 . 2
16 eqidd 2405 . 2
17 diblss.s . . 3
1817a1i 11 . 2
19 diblss.b . . . 4
20 diblss.l . . . 4
21 diblss.i . . . 4
2219, 20, 2, 21, 4, 11dibss 31652 . . 3
2322, 14sseqtr4d 3345 . 2
2419, 20, 2, 21dibn0 31636 . 2
25 fvex 5701 . . . . . . 7
26 vex 2919 . . . . . . . 8
27 fvex 5701 . . . . . . . 8
2826, 27coex 5372 . . . . . . 7
2925, 28op1st 6314 . . . . . 6
3029coeq1i 4991 . . . . 5
31 simpll 731 . . . . . . 7
32 simpr1 963 . . . . . . . 8
33 simplr 732 . . . . . . . . 9
34 simpr2 964 . . . . . . . . 9
3519, 20, 2, 10, 21dibelval1st1 31633 . . . . . . . . 9
3631, 33, 34, 35syl3anc 1184 . . . . . . . 8
372, 10, 3tendocl 31249 . . . . . . . 8
3831, 32, 36, 37syl3anc 1184 . . . . . . 7
39 simpr3 965 . . . . . . . 8
4019, 20, 2, 10, 21dibelval1st1 31633 . . . . . . . 8
4131, 33, 39, 40syl3anc 1184 . . . . . . 7
422, 10ltrnco 31201 . . . . . . 7
4331, 38, 41, 42syl3anc 1184 . . . . . 6
44 simplll 735 . . . . . . . 8
45 hllat 29846 . . . . . . . 8
4644, 45syl 16 . . . . . . 7
47 eqid 2404 . . . . . . . . 9
4819, 2, 10, 47trlcl 30646 . . . . . . . 8
4931, 43, 48syl2anc 643 . . . . . . 7
5019, 2, 10, 47trlcl 30646 . . . . . . . . 9
5131, 38, 50syl2anc 643 . . . . . . . 8
5219, 2, 10, 47trlcl 30646 . . . . . . . . 9
5331, 41, 52syl2anc 643 . . . . . . . 8
54 eqid 2404 . . . . . . . . 9
5519, 54latjcl 14434 . . . . . . . 8
5646, 51, 53, 55syl3anc 1184 . . . . . . 7
57 simplrl 737 . . . . . . 7
5820, 54, 2, 10, 47trlco 31209 . . . . . . . 8
5931, 38, 41, 58syl3anc 1184 . . . . . . 7
6019, 2, 10, 47trlcl 30646 . . . . . . . . . 10
6131, 36, 60syl2anc 643 . . . . . . . . 9
6220, 2, 10, 47, 3tendotp 31243 . . . . . . . . . 10
6331, 32, 36, 62syl3anc 1184 . . . . . . . . 9
64 eqid 2404 . . . . . . . . . . . 12
6519, 20, 2, 64, 21dibelval1st 31632 . . . . . . . . . . 11
6631, 33, 34, 65syl3anc 1184 . . . . . . . . . 10
6719, 20, 2, 10, 47, 64diatrl 31527 . . . . . . . . . 10
6831, 33, 66, 67syl3anc 1184 . . . . . . . . 9
6919, 20, 46, 51, 61, 57, 63, 68lattrd 14442 . . . . . . . 8
7019, 20, 2, 64, 21dibelval1st 31632 . . . . . . . . . 10
7131, 33, 39, 70syl3anc 1184 . . . . . . . . 9
7219, 20, 2, 10, 47, 64diatrl 31527 . . . . . . . . 9
7331, 33, 71, 72syl3anc 1184 . . . . . . . 8
7419, 20, 54latjle12 14446 . . . . . . . . 9
7546, 51, 53, 57, 74syl13anc 1186 . . . . . . . 8
7669, 73, 75mpbi2and 888 . . . . . . 7
7719, 20, 46, 49, 56, 57, 59, 76lattrd 14442 . . . . . 6
7819, 20, 2, 10, 47, 64diaelval 31516 . . . . . . 7
7978adantr 452 . . . . . 6
8043, 77, 79mpbir2and 889 . . . . 5
8130, 80syl5eqel 2488 . . . 4
82 eqid 2404 . . . . . . . . 9
83 eqid 2404 . . . . . . . . 9 Scalar Scalar
842, 10, 3, 4, 5, 82, 83dvhfplusr 31567 . . . . . . . 8 Scalar
8584ad2antrr 707 . . . . . . 7 Scalar
8625, 28op2nd 6315 . . . . . . . 8
87 eqid 2404 . . . . . . . . . . . 12
8819, 20, 2, 10, 87, 21dibelval2nd 31635 . . . . . . . . . . 11
8931, 33, 34, 88syl3anc 1184 . . . . . . . . . 10
9089coeq2d 4994 . . . . . . . . 9
9119, 2, 10, 3, 87tendo0mulr 31309 . . . . . . . . . 10
9231, 32, 91syl2anc 643 . . . . . . . . 9
9390, 92eqtrd 2436 . . . . . . . 8
9486, 93syl5eq 2448 . . . . . . 7
9519, 20, 2, 10, 87, 21dibelval2nd 31635 . . . . . . . 8
9631, 33, 39, 95syl3anc 1184 . . . . . . 7
9785, 94, 96oveq123d 6061 . . . . . 6 Scalar
98 simpllr 736 . . . . . . 7
9919, 2, 10, 3, 87tendo0cl 31272 . . . . . . . 8
10099ad2antrr 707 . . . . . . 7
10119, 2, 10, 3, 87, 82tendo0pl 31273 . . . . . . 7
10244, 98, 100, 101syl21anc 1183 . . . . . 6
10397, 102eqtrd 2436 . . . . 5 Scalar
104 ovex 6065 . . . . . 6 Scalar
105104elsnc 3797 . . . . 5 Scalar Scalar
106103, 105sylibr 204 . . . 4 Scalar
107 opelxpi 4869 . . . 4 Scalar Scalar
10881, 106, 107syl2anc 643 . . 3 Scalar
10923adantr 452 . . . . . . 7
110109, 34sseldd 3309 . . . . . 6
111 eqid 2404 . . . . . . 7
1122, 10, 3, 4, 111dvhvsca 31584 . . . . . 6
11331, 32, 110, 112syl12anc 1182 . . . . 5
114113oveq1d 6055 . . . 4
11589, 100eqeltrd 2478 . . . . . . 7
1162, 3tendococl 31254 . . . . . . 7
11731, 32, 115, 116syl3anc 1184 . . . . . 6
118 opelxpi 4869 . . . . . 6
11938, 117, 118syl2anc 643 . . . . 5
120109, 39sseldd 3309 . . . . 5
121 eqid 2404 . . . . . 6
1222, 10, 3, 4, 5, 121, 83dvhvadd 31575 . . . . 5 Scalar
12331, 119, 120, 122syl12anc 1182 . . . 4 Scalar
124114, 123eqtrd 2436 . . 3 Scalar
12519, 20, 2, 10, 87, 64, 21dibval2 31627 . . . 4