Metamath Proof Explorer


Theorem cdlemm10N

Description: The image of the map G is the entire one-dimensional subspace ( IV ) . Remark after Lemma M of Crawley p. 121 line 23. (Contributed by NM, 24-Nov-2013) (New usage is discouraged.)

Ref Expression
Hypotheses cdlemm10.l ˙ = K
cdlemm10.j ˙ = join K
cdlemm10.a A = Atoms K
cdlemm10.h H = LHyp K
cdlemm10.t T = LTrn K W
cdlemm10.r R = trL K W
cdlemm10.i I = DIsoA K W
cdlemm10.c C = r A | r ˙ P ˙ V ¬ r ˙ W
cdlemm10.f F = ι f T | f P = s
cdlemm10.g G = q C ι f T | f P = q
Assertion cdlemm10N K HL W H P A ¬ P ˙ W V A V ˙ W ran G = I V

Proof

Step Hyp Ref Expression
1 cdlemm10.l ˙ = K
2 cdlemm10.j ˙ = join K
3 cdlemm10.a A = Atoms K
4 cdlemm10.h H = LHyp K
5 cdlemm10.t T = LTrn K W
6 cdlemm10.r R = trL K W
7 cdlemm10.i I = DIsoA K W
8 cdlemm10.c C = r A | r ˙ P ˙ V ¬ r ˙ W
9 cdlemm10.f F = ι f T | f P = s
10 cdlemm10.g G = q C ι f T | f P = q
11 riotaex ι f T | f P = q V
12 11 10 fnmpti G Fn C
13 fvelrnb G Fn C g ran G s C G s = g
14 12 13 ax-mp g ran G s C G s = g
15 eqeq2 q = s f P = q f P = s
16 15 riotabidv q = s ι f T | f P = q = ι f T | f P = s
17 riotaex ι f T | f P = s V
18 16 10 17 fvmpt s C G s = ι f T | f P = s
19 18 9 eqtr4di s C G s = F
20 19 adantl K HL W H P A ¬ P ˙ W V A V ˙ W s C G s = F
21 20 eqeq1d K HL W H P A ¬ P ˙ W V A V ˙ W s C G s = g F = g
22 21 rexbidva K HL W H P A ¬ P ˙ W V A V ˙ W s C G s = g s C F = g
23 simpl1 K HL W H P A ¬ P ˙ W V A V ˙ W g T R g ˙ V K HL W H
24 simprl K HL W H P A ¬ P ˙ W V A V ˙ W g T R g ˙ V g T
25 simpl2l K HL W H P A ¬ P ˙ W V A V ˙ W g T R g ˙ V P A
26 1 3 4 5 ltrnat K HL W H g T P A g P A
27 23 24 25 26 syl3anc K HL W H P A ¬ P ˙ W V A V ˙ W g T R g ˙ V g P A
28 eqid Base K = Base K
29 simpl1l K HL W H P A ¬ P ˙ W V A V ˙ W g T R g ˙ V K HL
30 29 hllatd K HL W H P A ¬ P ˙ W V A V ˙ W g T R g ˙ V K Lat
31 28 3 atbase P A P Base K
32 25 31 syl K HL W H P A ¬ P ˙ W V A V ˙ W g T R g ˙ V P Base K
33 28 4 5 ltrncl K HL W H g T P Base K g P Base K
34 23 24 32 33 syl3anc K HL W H P A ¬ P ˙ W V A V ˙ W g T R g ˙ V g P Base K
35 28 2 latjcl K Lat P Base K g P Base K P ˙ g P Base K
36 30 32 34 35 syl3anc K HL W H P A ¬ P ˙ W V A V ˙ W g T R g ˙ V P ˙ g P Base K
37 simpl3l K HL W H P A ¬ P ˙ W V A V ˙ W g T R g ˙ V V A
38 28 2 3 hlatjcl K HL P A V A P ˙ V Base K
39 29 25 37 38 syl3anc K HL W H P A ¬ P ˙ W V A V ˙ W g T R g ˙ V P ˙ V Base K
40 28 1 2 latlej2 K Lat P Base K g P Base K g P ˙ P ˙ g P
41 30 32 34 40 syl3anc K HL W H P A ¬ P ˙ W V A V ˙ W g T R g ˙ V g P ˙ P ˙ g P
42 simpl2 K HL W H P A ¬ P ˙ W V A V ˙ W g T R g ˙ V P A ¬ P ˙ W
43 1 2 3 4 5 6 trljat1 K HL W H g T P A ¬ P ˙ W P ˙ R g = P ˙ g P
44 23 24 42 43 syl3anc K HL W H P A ¬ P ˙ W V A V ˙ W g T R g ˙ V P ˙ R g = P ˙ g P
45 simprr K HL W H P A ¬ P ˙ W V A V ˙ W g T R g ˙ V R g ˙ V
46 28 4 5 6 trlcl K HL W H g T R g Base K
47 23 24 46 syl2anc K HL W H P A ¬ P ˙ W V A V ˙ W g T R g ˙ V R g Base K
48 28 3 atbase V A V Base K
49 37 48 syl K HL W H P A ¬ P ˙ W V A V ˙ W g T R g ˙ V V Base K
50 28 1 2 latjlej2 K Lat R g Base K V Base K P Base K R g ˙ V P ˙ R g ˙ P ˙ V
51 30 47 49 32 50 syl13anc K HL W H P A ¬ P ˙ W V A V ˙ W g T R g ˙ V R g ˙ V P ˙ R g ˙ P ˙ V
52 45 51 mpd K HL W H P A ¬ P ˙ W V A V ˙ W g T R g ˙ V P ˙ R g ˙ P ˙ V
53 44 52 eqbrtrrd K HL W H P A ¬ P ˙ W V A V ˙ W g T R g ˙ V P ˙ g P ˙ P ˙ V
54 28 1 30 34 36 39 41 53 lattrd K HL W H P A ¬ P ˙ W V A V ˙ W g T R g ˙ V g P ˙ P ˙ V
55 1 3 4 5 ltrnel K HL W H g T P A ¬ P ˙ W g P A ¬ g P ˙ W
56 55 simprd K HL W H g T P A ¬ P ˙ W ¬ g P ˙ W
57 23 24 42 56 syl3anc K HL W H P A ¬ P ˙ W V A V ˙ W g T R g ˙ V ¬ g P ˙ W
58 54 57 jca K HL W H P A ¬ P ˙ W V A V ˙ W g T R g ˙ V g P ˙ P ˙ V ¬ g P ˙ W
59 breq1 r = g P r ˙ P ˙ V g P ˙ P ˙ V
60 breq1 r = g P r ˙ W g P ˙ W
61 60 notbid r = g P ¬ r ˙ W ¬ g P ˙ W
62 59 61 anbi12d r = g P r ˙ P ˙ V ¬ r ˙ W g P ˙ P ˙ V ¬ g P ˙ W
63 62 8 elrab2 g P C g P A g P ˙ P ˙ V ¬ g P ˙ W
64 27 58 63 sylanbrc K HL W H P A ¬ P ˙ W V A V ˙ W g T R g ˙ V g P C
65 1 3 4 5 cdlemeiota K HL W H P A ¬ P ˙ W g T g = ι f T | f P = g P
66 23 42 24 65 syl3anc K HL W H P A ¬ P ˙ W V A V ˙ W g T R g ˙ V g = ι f T | f P = g P
67 66 eqcomd K HL W H P A ¬ P ˙ W V A V ˙ W g T R g ˙ V ι f T | f P = g P = g
68 eqeq2 s = g P f P = s f P = g P
69 68 riotabidv s = g P ι f T | f P = s = ι f T | f P = g P
70 9 69 syl5eq s = g P F = ι f T | f P = g P
71 70 eqeq1d s = g P F = g ι f T | f P = g P = g
72 71 rspcev g P C ι f T | f P = g P = g s C F = g
73 64 67 72 syl2anc K HL W H P A ¬ P ˙ W V A V ˙ W g T R g ˙ V s C F = g
74 73 ex K HL W H P A ¬ P ˙ W V A V ˙ W g T R g ˙ V s C F = g
75 breq1 r = s r ˙ P ˙ V s ˙ P ˙ V
76 breq1 r = s r ˙ W s ˙ W
77 76 notbid r = s ¬ r ˙ W ¬ s ˙ W
78 75 77 anbi12d r = s r ˙ P ˙ V ¬ r ˙ W s ˙ P ˙ V ¬ s ˙ W
79 78 8 elrab2 s C s A s ˙ P ˙ V ¬ s ˙ W
80 simpl1 K HL W H P A ¬ P ˙ W V A V ˙ W s A s ˙ P ˙ V ¬ s ˙ W K HL W H
81 simpl2l K HL W H P A ¬ P ˙ W V A V ˙ W s A s ˙ P ˙ V ¬ s ˙ W P A
82 simpl2r K HL W H P A ¬ P ˙ W V A V ˙ W s A s ˙ P ˙ V ¬ s ˙ W ¬ P ˙ W
83 simprl K HL W H P A ¬ P ˙ W V A V ˙ W s A s ˙ P ˙ V ¬ s ˙ W s A
84 simprrr K HL W H P A ¬ P ˙ W V A V ˙ W s A s ˙ P ˙ V ¬ s ˙ W ¬ s ˙ W
85 1 3 4 5 9 ltrniotacl K HL W H P A ¬ P ˙ W s A ¬ s ˙ W F T
86 1 3 4 5 9 ltrniotaval K HL W H P A ¬ P ˙ W s A ¬ s ˙ W F P = s
87 85 86 jca K HL W H P A ¬ P ˙ W s A ¬ s ˙ W F T F P = s
88 80 81 82 83 84 87 syl122anc K HL W H P A ¬ P ˙ W V A V ˙ W s A s ˙ P ˙ V ¬ s ˙ W F T F P = s
89 simp3l K HL W H P A ¬ P ˙ W V A V ˙ W s A s ˙ P ˙ V ¬ s ˙ W F T F P = s F T
90 simp11 K HL W H P A ¬ P ˙ W V A V ˙ W s A s ˙ P ˙ V ¬ s ˙ W F T F P = s K HL W H
91 simp12 K HL W H P A ¬ P ˙ W V A V ˙ W s A s ˙ P ˙ V ¬ s ˙ W F T F P = s P A ¬ P ˙ W
92 eqid meet K = meet K
93 1 2 92 3 4 5 6 trlval2 K HL W H F T P A ¬ P ˙ W R F = P ˙ F P meet K W
94 90 89 91 93 syl3anc K HL W H P A ¬ P ˙ W V A V ˙ W s A s ˙ P ˙ V ¬ s ˙ W F T F P = s R F = P ˙ F P meet K W
95 simp3r K HL W H P A ¬ P ˙ W V A V ˙ W s A s ˙ P ˙ V ¬ s ˙ W F T F P = s F P = s
96 95 oveq2d K HL W H P A ¬ P ˙ W V A V ˙ W s A s ˙ P ˙ V ¬ s ˙ W F T F P = s P ˙ F P = P ˙ s
97 96 oveq1d K HL W H P A ¬ P ˙ W V A V ˙ W s A s ˙ P ˙ V ¬ s ˙ W F T F P = s P ˙ F P meet K W = P ˙ s meet K W
98 94 97 eqtrd K HL W H P A ¬ P ˙ W V A V ˙ W s A s ˙ P ˙ V ¬ s ˙ W F T F P = s R F = P ˙ s meet K W
99 simpl1l K HL W H P A ¬ P ˙ W V A V ˙ W s A s ˙ P ˙ V ¬ s ˙ W K HL
100 simpl3l K HL W H P A ¬ P ˙ W V A V ˙ W s A s ˙ P ˙ V ¬ s ˙ W V A
101 1 2 3 hlatlej1 K HL P A V A P ˙ P ˙ V
102 99 81 100 101 syl3anc K HL W H P A ¬ P ˙ W V A V ˙ W s A s ˙ P ˙ V ¬ s ˙ W P ˙ P ˙ V
103 simprrl K HL W H P A ¬ P ˙ W V A V ˙ W s A s ˙ P ˙ V ¬ s ˙ W s ˙ P ˙ V
104 99 hllatd K HL W H P A ¬ P ˙ W V A V ˙ W s A s ˙ P ˙ V ¬ s ˙ W K Lat
105 81 31 syl K HL W H P A ¬ P ˙ W V A V ˙ W s A s ˙ P ˙ V ¬ s ˙ W P Base K
106 28 3 atbase s A s Base K
107 106 ad2antrl K HL W H P A ¬ P ˙ W V A V ˙ W s A s ˙ P ˙ V ¬ s ˙ W s Base K
108 99 81 100 38 syl3anc K HL W H P A ¬ P ˙ W V A V ˙ W s A s ˙ P ˙ V ¬ s ˙ W P ˙ V Base K
109 28 1 2 latjle12 K Lat P Base K s Base K P ˙ V Base K P ˙ P ˙ V s ˙ P ˙ V P ˙ s ˙ P ˙ V
110 104 105 107 108 109 syl13anc K HL W H P A ¬ P ˙ W V A V ˙ W s A s ˙ P ˙ V ¬ s ˙ W P ˙ P ˙ V s ˙ P ˙ V P ˙ s ˙ P ˙ V
111 102 103 110 mpbi2and K HL W H P A ¬ P ˙ W V A V ˙ W s A s ˙ P ˙ V ¬ s ˙ W P ˙ s ˙ P ˙ V
112 28 2 3 hlatjcl K HL P A s A P ˙ s Base K
113 99 81 83 112 syl3anc K HL W H P A ¬ P ˙ W V A V ˙ W s A s ˙ P ˙ V ¬ s ˙ W P ˙ s Base K
114 simpl1r K HL W H P A ¬ P ˙ W V A V ˙ W s A s ˙ P ˙ V ¬ s ˙ W W H
115 28 4 lhpbase W H W Base K
116 114 115 syl K HL W H P A ¬ P ˙ W V A V ˙ W s A s ˙ P ˙ V ¬ s ˙ W W Base K
117 28 1 92 latmlem1 K Lat P ˙ s Base K P ˙ V Base K W Base K P ˙ s ˙ P ˙ V P ˙ s meet K W ˙ P ˙ V meet K W
118 104 113 108 116 117 syl13anc K HL W H P A ¬ P ˙ W V A V ˙ W s A s ˙ P ˙ V ¬ s ˙ W P ˙ s ˙ P ˙ V P ˙ s meet K W ˙ P ˙ V meet K W
119 111 118 mpd K HL W H P A ¬ P ˙ W V A V ˙ W s A s ˙ P ˙ V ¬ s ˙ W P ˙ s meet K W ˙ P ˙ V meet K W
120 1 2 92 3 4 lhpat4N K HL W H P A ¬ P ˙ W V A V ˙ W P ˙ V meet K W = V
121 120 adantr K HL W H P A ¬ P ˙ W V A V ˙ W s A s ˙ P ˙ V ¬ s ˙ W P ˙ V meet K W = V
122 119 121 breqtrd K HL W H P A ¬ P ˙ W V A V ˙ W s A s ˙ P ˙ V ¬ s ˙ W P ˙ s meet K W ˙ V
123 122 3adant3 K HL W H P A ¬ P ˙ W V A V ˙ W s A s ˙ P ˙ V ¬ s ˙ W F T F P = s P ˙ s meet K W ˙ V
124 98 123 eqbrtrd K HL W H P A ¬ P ˙ W V A V ˙ W s A s ˙ P ˙ V ¬ s ˙ W F T F P = s R F ˙ V
125 89 124 jca K HL W H P A ¬ P ˙ W V A V ˙ W s A s ˙ P ˙ V ¬ s ˙ W F T F P = s F T R F ˙ V
126 88 125 mpd3an3 K HL W H P A ¬ P ˙ W V A V ˙ W s A s ˙ P ˙ V ¬ s ˙ W F T R F ˙ V
127 79 126 sylan2b K HL W H P A ¬ P ˙ W V A V ˙ W s C F T R F ˙ V
128 127 ex K HL W H P A ¬ P ˙ W V A V ˙ W s C F T R F ˙ V
129 eleq1 F = g F T g T
130 fveq2 F = g R F = R g
131 130 breq1d F = g R F ˙ V R g ˙ V
132 129 131 anbi12d F = g F T R F ˙ V g T R g ˙ V
133 132 biimpcd F T R F ˙ V F = g g T R g ˙ V
134 128 133 syl6 K HL W H P A ¬ P ˙ W V A V ˙ W s C F = g g T R g ˙ V
135 134 rexlimdv K HL W H P A ¬ P ˙ W V A V ˙ W s C F = g g T R g ˙ V
136 74 135 impbid K HL W H P A ¬ P ˙ W V A V ˙ W g T R g ˙ V s C F = g
137 22 136 bitr4d K HL W H P A ¬ P ˙ W V A V ˙ W s C G s = g g T R g ˙ V
138 fveq2 f = g R f = R g
139 138 breq1d f = g R f ˙ V R g ˙ V
140 139 elrab g f T | R f ˙ V g T R g ˙ V
141 137 140 bitr4di K HL W H P A ¬ P ˙ W V A V ˙ W s C G s = g g f T | R f ˙ V
142 simp1l K HL W H P A ¬ P ˙ W V A V ˙ W K HL
143 simp1r K HL W H P A ¬ P ˙ W V A V ˙ W W H
144 simp3l K HL W H P A ¬ P ˙ W V A V ˙ W V A
145 144 48 syl K HL W H P A ¬ P ˙ W V A V ˙ W V Base K
146 simp3r K HL W H P A ¬ P ˙ W V A V ˙ W V ˙ W
147 28 1 4 5 6 7 diaval K HL W H V Base K V ˙ W I V = f T | R f ˙ V
148 142 143 145 146 147 syl22anc K HL W H P A ¬ P ˙ W V A V ˙ W I V = f T | R f ˙ V
149 148 eleq2d K HL W H P A ¬ P ˙ W V A V ˙ W g I V g f T | R f ˙ V
150 141 149 bitr4d K HL W H P A ¬ P ˙ W V A V ˙ W s C G s = g g I V
151 14 150 syl5bb K HL W H P A ¬ P ˙ W V A V ˙ W g ran G g I V
152 151 eqrdv K HL W H P A ¬ P ˙ W V A V ˙ W ran G = I V