Metamath Proof Explorer


Theorem dihmeetlem4preN

Description: Lemma for isomorphism H of a lattice meet. (Contributed by NM, 30-Mar-2014) (New usage is discouraged.)

Ref Expression
Hypotheses dihmeetlem4.b B = Base K
dihmeetlem4.l ˙ = K
dihmeetlem4.m ˙ = meet K
dihmeetlem4.a A = Atoms K
dihmeetlem4.h H = LHyp K
dihmeetlem4.i I = DIsoH K W
dihmeetlem4.u U = DVecH K W
dihmeetlem4.z 0 ˙ = 0 U
dihmeetlem4.g G = ι g T | g P = Q
dihmeetlem4.p P = oc K W
dihmeetlem4.t T = LTrn K W
dihmeetlem4.r R = trL K W
dihmeetlem4.e E = TEndo K W
dihmeetlem4.o O = h T I B
Assertion dihmeetlem4preN K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W I Q I X ˙ W = 0 ˙

Proof

Step Hyp Ref Expression
1 dihmeetlem4.b B = Base K
2 dihmeetlem4.l ˙ = K
3 dihmeetlem4.m ˙ = meet K
4 dihmeetlem4.a A = Atoms K
5 dihmeetlem4.h H = LHyp K
6 dihmeetlem4.i I = DIsoH K W
7 dihmeetlem4.u U = DVecH K W
8 dihmeetlem4.z 0 ˙ = 0 U
9 dihmeetlem4.g G = ι g T | g P = Q
10 dihmeetlem4.p P = oc K W
11 dihmeetlem4.t T = LTrn K W
12 dihmeetlem4.r R = trL K W
13 dihmeetlem4.e E = TEndo K W
14 dihmeetlem4.o O = h T I B
15 5 6 dihvalrel K HL W H Rel I Q
16 relin1 Rel I Q Rel I Q I X ˙ W
17 15 16 syl K HL W H Rel I Q I X ˙ W
18 17 3ad2ant1 K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Rel I Q I X ˙ W
19 5 6 dihvalrel K HL W H Rel I 0. K
20 eqid 0. K = 0. K
21 20 5 6 7 8 dih0 K HL W H I 0. K = 0 ˙
22 21 releqd K HL W H Rel I 0. K Rel 0 ˙
23 19 22 mpbid K HL W H Rel 0 ˙
24 23 3ad2ant1 K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Rel 0 ˙
25 id K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W
26 elin f s I Q I X ˙ W f s I Q f s I X ˙ W
27 vex f V
28 vex s V
29 2 4 5 10 11 13 6 9 27 28 dihopelvalcqat K HL W H Q A ¬ Q ˙ W f s I Q f = s G s E
30 29 3adant2 K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W f s I Q f = s G s E
31 simp1 K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W K HL W H
32 simp1l K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W K HL
33 32 hllatd K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W K Lat
34 simp2l K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W X B
35 simp1r K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W W H
36 1 5 lhpbase W H W B
37 35 36 syl K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W W B
38 1 3 latmcl K Lat X B W B X ˙ W B
39 33 34 37 38 syl3anc K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W X ˙ W B
40 1 2 3 latmle2 K Lat X B W B X ˙ W ˙ W
41 33 34 37 40 syl3anc K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W X ˙ W ˙ W
42 1 2 5 11 12 14 6 dihopelvalbN K HL W H X ˙ W B X ˙ W ˙ W f s I X ˙ W f T R f ˙ X ˙ W s = O
43 31 39 41 42 syl12anc K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W f s I X ˙ W f T R f ˙ X ˙ W s = O
44 30 43 anbi12d K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W f s I Q f s I X ˙ W f = s G s E f T R f ˙ X ˙ W s = O
45 simprll K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W f = s G s E f T R f ˙ X ˙ W s = O f = s G
46 simprrr K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W f = s G s E f T R f ˙ X ˙ W s = O s = O
47 46 fveq1d K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W f = s G s E f T R f ˙ X ˙ W s = O s G = O G
48 simpl1 K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W f = s G s E f T R f ˙ X ˙ W s = O K HL W H
49 2 4 5 10 lhpocnel2 K HL W H P A ¬ P ˙ W
50 48 49 syl K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W f = s G s E f T R f ˙ X ˙ W s = O P A ¬ P ˙ W
51 simpl3 K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W f = s G s E f T R f ˙ X ˙ W s = O Q A ¬ Q ˙ W
52 2 4 5 11 9 ltrniotacl K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W G T
53 48 50 51 52 syl3anc K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W f = s G s E f T R f ˙ X ˙ W s = O G T
54 14 1 tendo02 G T O G = I B
55 53 54 syl K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W f = s G s E f T R f ˙ X ˙ W s = O O G = I B
56 45 47 55 3eqtrd K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W f = s G s E f T R f ˙ X ˙ W s = O f = I B
57 56 46 jca K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W f = s G s E f T R f ˙ X ˙ W s = O f = I B s = O
58 simpl1 K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W f = I B s = O K HL W H
59 58 49 syl K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W f = I B s = O P A ¬ P ˙ W
60 simpl3 K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W f = I B s = O Q A ¬ Q ˙ W
61 58 59 60 52 syl3anc K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W f = I B s = O G T
62 61 54 syl K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W f = I B s = O O G = I B
63 simprr K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W f = I B s = O s = O
64 63 fveq1d K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W f = I B s = O s G = O G
65 simprl K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W f = I B s = O f = I B
66 62 64 65 3eqtr4rd K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W f = I B s = O f = s G
67 1 5 11 13 14 tendo0cl K HL W H O E
68 58 67 syl K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W f = I B s = O O E
69 63 68 eqeltrd K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W f = I B s = O s E
70 1 5 11 idltrn K HL W H I B T
71 58 70 syl K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W f = I B s = O I B T
72 65 71 eqeltrd K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W f = I B s = O f T
73 65 fveq2d K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W f = I B s = O R f = R I B
74 1 20 5 12 trlid0 K HL W H R I B = 0. K
75 58 74 syl K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W f = I B s = O R I B = 0. K
76 73 75 eqtrd K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W f = I B s = O R f = 0. K
77 simpl1l K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W f = I B s = O K HL
78 hlatl K HL K AtLat
79 77 78 syl K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W f = I B s = O K AtLat
80 39 adantr K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W f = I B s = O X ˙ W B
81 1 2 20 atl0le K AtLat X ˙ W B 0. K ˙ X ˙ W
82 79 80 81 syl2anc K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W f = I B s = O 0. K ˙ X ˙ W
83 76 82 eqbrtrd K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W f = I B s = O R f ˙ X ˙ W
84 72 83 63 jca31 K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W f = I B s = O f T R f ˙ X ˙ W s = O
85 66 69 84 jca31 K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W f = I B s = O f = s G s E f T R f ˙ X ˙ W s = O
86 57 85 impbida K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W f = s G s E f T R f ˙ X ˙ W s = O f = I B s = O
87 44 86 bitrd K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W f s I Q f s I X ˙ W f = I B s = O
88 opex f s V
89 88 elsn f s I B O f s = I B O
90 27 28 opth f s = I B O f = I B s = O
91 89 90 bitr2i f = I B s = O f s I B O
92 87 91 bitrdi K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W f s I Q f s I X ˙ W f s I B O
93 1 5 11 7 8 14 dvh0g K HL W H 0 ˙ = I B O
94 93 3ad2ant1 K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W 0 ˙ = I B O
95 94 sneqd K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W 0 ˙ = I B O
96 95 eleq2d K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W f s 0 ˙ f s I B O
97 92 96 bitr4d K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W f s I Q f s I X ˙ W f s 0 ˙
98 26 97 syl5bb K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W f s I Q I X ˙ W f s 0 ˙
99 98 eqrelrdv2 Rel I Q I X ˙ W Rel 0 ˙ K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W I Q I X ˙ W = 0 ˙
100 18 24 25 99 syl21anc K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W I Q I X ˙ W = 0 ˙