Metamath Proof Explorer


Theorem djajN

Description: Transfer lattice join to DVecA partial vector space closed subspace join. Part of Lemma M of Crawley p. 120 line 29, with closed subspace join rather than subspace sum. (Contributed by NM, 5-Dec-2013) (New usage is discouraged.)

Ref Expression
Hypotheses djaj.k ˙ = join K
djaj.h H = LHyp K
djaj.i I = DIsoA K W
djaj.j J = vA K W
Assertion djajN K HL W H X dom I Y dom I I X ˙ Y = I X J I Y

Proof

Step Hyp Ref Expression
1 djaj.k ˙ = join K
2 djaj.h H = LHyp K
3 djaj.i I = DIsoA K W
4 djaj.j J = vA K W
5 hllat K HL K Lat
6 5 ad2antrr K HL W H X dom I Y dom I K Lat
7 hlop K HL K OP
8 7 ad2antrr K HL W H X dom I Y dom I K OP
9 eqid Base K = Base K
10 9 2 3 diadmclN K HL W H X dom I X Base K
11 10 adantrr K HL W H X dom I Y dom I X Base K
12 eqid oc K = oc K
13 9 12 opoccl K OP X Base K oc K X Base K
14 8 11 13 syl2anc K HL W H X dom I Y dom I oc K X Base K
15 9 2 lhpbase W H W Base K
16 15 ad2antlr K HL W H X dom I Y dom I W Base K
17 9 12 opoccl K OP W Base K oc K W Base K
18 8 16 17 syl2anc K HL W H X dom I Y dom I oc K W Base K
19 9 1 latjcl K Lat oc K X Base K oc K W Base K oc K X ˙ oc K W Base K
20 6 14 18 19 syl3anc K HL W H X dom I Y dom I oc K X ˙ oc K W Base K
21 eqid meet K = meet K
22 9 21 latmcl K Lat oc K X ˙ oc K W Base K W Base K oc K X ˙ oc K W meet K W Base K
23 6 20 16 22 syl3anc K HL W H X dom I Y dom I oc K X ˙ oc K W meet K W Base K
24 9 2 3 diadmclN K HL W H Y dom I Y Base K
25 24 adantrl K HL W H X dom I Y dom I Y Base K
26 9 12 opoccl K OP Y Base K oc K Y Base K
27 8 25 26 syl2anc K HL W H X dom I Y dom I oc K Y Base K
28 9 1 latjcl K Lat oc K Y Base K oc K W Base K oc K Y ˙ oc K W Base K
29 6 27 18 28 syl3anc K HL W H X dom I Y dom I oc K Y ˙ oc K W Base K
30 9 21 latmcl K Lat oc K Y ˙ oc K W Base K W Base K oc K Y ˙ oc K W meet K W Base K
31 6 29 16 30 syl3anc K HL W H X dom I Y dom I oc K Y ˙ oc K W meet K W Base K
32 9 21 latmcl K Lat oc K X ˙ oc K W meet K W Base K oc K Y ˙ oc K W meet K W Base K oc K X ˙ oc K W meet K W meet K oc K Y ˙ oc K W meet K W Base K
33 6 23 31 32 syl3anc K HL W H X dom I Y dom I oc K X ˙ oc K W meet K W meet K oc K Y ˙ oc K W meet K W Base K
34 eqid K = K
35 9 34 21 latmle2 K Lat oc K X ˙ oc K W meet K W Base K oc K Y ˙ oc K W meet K W Base K oc K X ˙ oc K W meet K W meet K oc K Y ˙ oc K W meet K W K oc K Y ˙ oc K W meet K W
36 6 23 31 35 syl3anc K HL W H X dom I Y dom I oc K X ˙ oc K W meet K W meet K oc K Y ˙ oc K W meet K W K oc K Y ˙ oc K W meet K W
37 9 34 21 latmle2 K Lat oc K Y ˙ oc K W Base K W Base K oc K Y ˙ oc K W meet K W K W
38 6 29 16 37 syl3anc K HL W H X dom I Y dom I oc K Y ˙ oc K W meet K W K W
39 9 34 6 33 31 16 36 38 lattrd K HL W H X dom I Y dom I oc K X ˙ oc K W meet K W meet K oc K Y ˙ oc K W meet K W K W
40 9 34 2 3 diaeldm K HL W H oc K X ˙ oc K W meet K W meet K oc K Y ˙ oc K W meet K W dom I oc K X ˙ oc K W meet K W meet K oc K Y ˙ oc K W meet K W Base K oc K X ˙ oc K W meet K W meet K oc K Y ˙ oc K W meet K W K W
41 40 adantr K HL W H X dom I Y dom I oc K X ˙ oc K W meet K W meet K oc K Y ˙ oc K W meet K W dom I oc K X ˙ oc K W meet K W meet K oc K Y ˙ oc K W meet K W Base K oc K X ˙ oc K W meet K W meet K oc K Y ˙ oc K W meet K W K W
42 33 39 41 mpbir2and K HL W H X dom I Y dom I oc K X ˙ oc K W meet K W meet K oc K Y ˙ oc K W meet K W dom I
43 eqid LTrn K W = LTrn K W
44 eqid ocA K W = ocA K W
45 1 21 12 2 43 3 44 diaocN K HL W H oc K X ˙ oc K W meet K W meet K oc K Y ˙ oc K W meet K W dom I I oc K oc K X ˙ oc K W meet K W meet K oc K Y ˙ oc K W meet K W ˙ oc K W meet K W = ocA K W I oc K X ˙ oc K W meet K W meet K oc K Y ˙ oc K W meet K W
46 42 45 syldan K HL W H X dom I Y dom I I oc K oc K X ˙ oc K W meet K W meet K oc K Y ˙ oc K W meet K W ˙ oc K W meet K W = ocA K W I oc K X ˙ oc K W meet K W meet K oc K Y ˙ oc K W meet K W
47 hloml K HL K OML
48 47 ad2antrr K HL W H X dom I Y dom I K OML
49 9 1 latjcl K Lat X Base K Y Base K X ˙ Y Base K
50 6 11 25 49 syl3anc K HL W H X dom I Y dom I X ˙ Y Base K
51 34 2 3 diadmleN K HL W H X dom I X K W
52 51 adantrr K HL W H X dom I Y dom I X K W
53 34 2 3 diadmleN K HL W H Y dom I Y K W
54 53 adantrl K HL W H X dom I Y dom I Y K W
55 9 34 1 latjle12 K Lat X Base K Y Base K W Base K X K W Y K W X ˙ Y K W
56 6 11 25 16 55 syl13anc K HL W H X dom I Y dom I X K W Y K W X ˙ Y K W
57 52 54 56 mpbi2and K HL W H X dom I Y dom I X ˙ Y K W
58 9 34 1 21 12 omlspjN K OML X ˙ Y Base K W Base K X ˙ Y K W X ˙ Y ˙ oc K W meet K W = X ˙ Y
59 48 50 16 57 58 syl121anc K HL W H X dom I Y dom I X ˙ Y ˙ oc K W meet K W = X ˙ Y
60 9 1 latjidm K Lat oc K W Base K oc K W ˙ oc K W = oc K W
61 6 18 60 syl2anc K HL W H X dom I Y dom I oc K W ˙ oc K W = oc K W
62 61 oveq2d K HL W H X dom I Y dom I X ˙ Y ˙ oc K W ˙ oc K W = X ˙ Y ˙ oc K W
63 9 1 latjass K Lat X ˙ Y Base K oc K W Base K oc K W Base K X ˙ Y ˙ oc K W ˙ oc K W = X ˙ Y ˙ oc K W ˙ oc K W
64 6 50 18 18 63 syl13anc K HL W H X dom I Y dom I X ˙ Y ˙ oc K W ˙ oc K W = X ˙ Y ˙ oc K W ˙ oc K W
65 hlol K HL K OL
66 65 ad2antrr K HL W H X dom I Y dom I K OL
67 9 1 21 12 oldmm2 K OL X ˙ Y Base K W Base K oc K oc K X ˙ Y meet K W = X ˙ Y ˙ oc K W
68 66 50 16 67 syl3anc K HL W H X dom I Y dom I oc K oc K X ˙ Y meet K W = X ˙ Y ˙ oc K W
69 9 1 21 12 oldmj1 K OL X Base K Y Base K oc K X ˙ Y = oc K X meet K oc K Y
70 66 11 25 69 syl3anc K HL W H X dom I Y dom I oc K X ˙ Y = oc K X meet K oc K Y
71 9 34 21 latleeqm1 K Lat X Base K W Base K X K W X meet K W = X
72 6 11 16 71 syl3anc K HL W H X dom I Y dom I X K W X meet K W = X
73 52 72 mpbid K HL W H X dom I Y dom I X meet K W = X
74 73 fveq2d K HL W H X dom I Y dom I oc K X meet K W = oc K X
75 9 1 21 12 oldmm1 K OL X Base K W Base K oc K X meet K W = oc K X ˙ oc K W
76 66 11 16 75 syl3anc K HL W H X dom I Y dom I oc K X meet K W = oc K X ˙ oc K W
77 74 76 eqtr3d K HL W H X dom I Y dom I oc K X = oc K X ˙ oc K W
78 9 34 21 latleeqm1 K Lat Y Base K W Base K Y K W Y meet K W = Y
79 6 25 16 78 syl3anc K HL W H X dom I Y dom I Y K W Y meet K W = Y
80 54 79 mpbid K HL W H X dom I Y dom I Y meet K W = Y
81 80 fveq2d K HL W H X dom I Y dom I oc K Y meet K W = oc K Y
82 9 1 21 12 oldmm1 K OL Y Base K W Base K oc K Y meet K W = oc K Y ˙ oc K W
83 66 25 16 82 syl3anc K HL W H X dom I Y dom I oc K Y meet K W = oc K Y ˙ oc K W
84 81 83 eqtr3d K HL W H X dom I Y dom I oc K Y = oc K Y ˙ oc K W
85 77 84 oveq12d K HL W H X dom I Y dom I oc K X meet K oc K Y = oc K X ˙ oc K W meet K oc K Y ˙ oc K W
86 70 85 eqtrd K HL W H X dom I Y dom I oc K X ˙ Y = oc K X ˙ oc K W meet K oc K Y ˙ oc K W
87 86 oveq1d K HL W H X dom I Y dom I oc K X ˙ Y meet K W = oc K X ˙ oc K W meet K oc K Y ˙ oc K W meet K W
88 9 21 latmmdir K OL oc K X ˙ oc K W Base K oc K Y ˙ oc K W Base K W Base K oc K X ˙ oc K W meet K oc K Y ˙ oc K W meet K W = oc K X ˙ oc K W meet K W meet K oc K Y ˙ oc K W meet K W
89 66 20 29 16 88 syl13anc K HL W H X dom I Y dom I oc K X ˙ oc K W meet K oc K Y ˙ oc K W meet K W = oc K X ˙ oc K W meet K W meet K oc K Y ˙ oc K W meet K W
90 87 89 eqtrd K HL W H X dom I Y dom I oc K X ˙ Y meet K W = oc K X ˙ oc K W meet K W meet K oc K Y ˙ oc K W meet K W
91 90 fveq2d K HL W H X dom I Y dom I oc K oc K X ˙ Y meet K W = oc K oc K X ˙ oc K W meet K W meet K oc K Y ˙ oc K W meet K W
92 68 91 eqtr3d K HL W H X dom I Y dom I X ˙ Y ˙ oc K W = oc K oc K X ˙ oc K W meet K W meet K oc K Y ˙ oc K W meet K W
93 92 oveq1d K HL W H X dom I Y dom I X ˙ Y ˙ oc K W ˙ oc K W = oc K oc K X ˙ oc K W meet K W meet K oc K Y ˙ oc K W meet K W ˙ oc K W
94 64 93 eqtr3d K HL W H X dom I Y dom I X ˙ Y ˙ oc K W ˙ oc K W = oc K oc K X ˙ oc K W meet K W meet K oc K Y ˙ oc K W meet K W ˙ oc K W
95 62 94 eqtr3d K HL W H X dom I Y dom I X ˙ Y ˙ oc K W = oc K oc K X ˙ oc K W meet K W meet K oc K Y ˙ oc K W meet K W ˙ oc K W
96 95 oveq1d K HL W H X dom I Y dom I X ˙ Y ˙ oc K W meet K W = oc K oc K X ˙ oc K W meet K W meet K oc K Y ˙ oc K W meet K W ˙ oc K W meet K W
97 59 96 eqtr3d K HL W H X dom I Y dom I X ˙ Y = oc K oc K X ˙ oc K W meet K W meet K oc K Y ˙ oc K W meet K W ˙ oc K W meet K W
98 97 fveq2d K HL W H X dom I Y dom I I X ˙ Y = I oc K oc K X ˙ oc K W meet K W meet K oc K Y ˙ oc K W meet K W ˙ oc K W meet K W
99 simpl K HL W H X dom I Y dom I K HL W H
100 2 3 diaclN K HL W H X dom I I X ran I
101 100 adantrr K HL W H X dom I Y dom I I X ran I
102 2 43 3 diaelrnN K HL W H I X ran I I X LTrn K W
103 101 102 syldan K HL W H X dom I Y dom I I X LTrn K W
104 2 3 diaclN K HL W H Y dom I I Y ran I
105 104 adantrl K HL W H X dom I Y dom I I Y ran I
106 2 43 3 diaelrnN K HL W H I Y ran I I Y LTrn K W
107 105 106 syldan K HL W H X dom I Y dom I I Y LTrn K W
108 2 43 3 44 4 djavalN K HL W H I X LTrn K W I Y LTrn K W I X J I Y = ocA K W ocA K W I X ocA K W I Y
109 99 103 107 108 syl12anc K HL W H X dom I Y dom I I X J I Y = ocA K W ocA K W I X ocA K W I Y
110 9 34 21 latmle2 K Lat oc K X ˙ oc K W Base K W Base K oc K X ˙ oc K W meet K W K W
111 6 20 16 110 syl3anc K HL W H X dom I Y dom I oc K X ˙ oc K W meet K W K W
112 9 34 2 3 diaeldm K HL W H oc K X ˙ oc K W meet K W dom I oc K X ˙ oc K W meet K W Base K oc K X ˙ oc K W meet K W K W
113 112 adantr K HL W H X dom I Y dom I oc K X ˙ oc K W meet K W dom I oc K X ˙ oc K W meet K W Base K oc K X ˙ oc K W meet K W K W
114 23 111 113 mpbir2and K HL W H X dom I Y dom I oc K X ˙ oc K W meet K W dom I
115 9 34 2 3 diaeldm K HL W H oc K Y ˙ oc K W meet K W dom I oc K Y ˙ oc K W meet K W Base K oc K Y ˙ oc K W meet K W K W
116 115 adantr K HL W H X dom I Y dom I oc K Y ˙ oc K W meet K W dom I oc K Y ˙ oc K W meet K W Base K oc K Y ˙ oc K W meet K W K W
117 31 38 116 mpbir2and K HL W H X dom I Y dom I oc K Y ˙ oc K W meet K W dom I
118 21 2 3 diameetN K HL W H oc K X ˙ oc K W meet K W dom I oc K Y ˙ oc K W meet K W dom I I oc K X ˙ oc K W meet K W meet K oc K Y ˙ oc K W meet K W = I oc K X ˙ oc K W meet K W I oc K Y ˙ oc K W meet K W
119 99 114 117 118 syl12anc K HL W H X dom I Y dom I I oc K X ˙ oc K W meet K W meet K oc K Y ˙ oc K W meet K W = I oc K X ˙ oc K W meet K W I oc K Y ˙ oc K W meet K W
120 1 21 12 2 43 3 44 diaocN K HL W H X dom I I oc K X ˙ oc K W meet K W = ocA K W I X
121 120 adantrr K HL W H X dom I Y dom I I oc K X ˙ oc K W meet K W = ocA K W I X
122 1 21 12 2 43 3 44 diaocN K HL W H Y dom I I oc K Y ˙ oc K W meet K W = ocA K W I Y
123 122 adantrl K HL W H X dom I Y dom I I oc K Y ˙ oc K W meet K W = ocA K W I Y
124 121 123 ineq12d K HL W H X dom I Y dom I I oc K X ˙ oc K W meet K W I oc K Y ˙ oc K W meet K W = ocA K W I X ocA K W I Y
125 119 124 eqtrd K HL W H X dom I Y dom I I oc K X ˙ oc K W meet K W meet K oc K Y ˙ oc K W meet K W = ocA K W I X ocA K W I Y
126 125 fveq2d K HL W H X dom I Y dom I ocA K W I oc K X ˙ oc K W meet K W meet K oc K Y ˙ oc K W meet K W = ocA K W ocA K W I X ocA K W I Y
127 109 126 eqtr4d K HL W H X dom I Y dom I I X J I Y = ocA K W I oc K X ˙ oc K W meet K W meet K oc K Y ˙ oc K W meet K W
128 46 98 127 3eqtr4d K HL W H X dom I Y dom I I X ˙ Y = I X J I Y