Metamath Proof Explorer


Theorem dihmeetlem13N

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

Ref Expression
Hypotheses dihmeetlem13.b B = Base K
dihmeetlem13.l ˙ = K
dihmeetlem13.j ˙ = join K
dihmeetlem13.a A = Atoms K
dihmeetlem13.h H = LHyp K
dihmeetlem13.p P = oc K W
dihmeetlem13.t T = LTrn K W
dihmeetlem13.e E = TEndo K W
dihmeetlem13.o O = h T I B
dihmeetlem13.i I = DIsoH K W
dihmeetlem13.u U = DVecH K W
dihmeetlem13.z 0 ˙ = 0 U
dihmeetlem13.f F = ι h T | h P = Q
dihmeetlem13.g G = ι h T | h P = R
Assertion dihmeetlem13N K HL W H Q A ¬ Q ˙ W R A ¬ R ˙ W Q R I Q I R = 0 ˙

Proof

Step Hyp Ref Expression
1 dihmeetlem13.b B = Base K
2 dihmeetlem13.l ˙ = K
3 dihmeetlem13.j ˙ = join K
4 dihmeetlem13.a A = Atoms K
5 dihmeetlem13.h H = LHyp K
6 dihmeetlem13.p P = oc K W
7 dihmeetlem13.t T = LTrn K W
8 dihmeetlem13.e E = TEndo K W
9 dihmeetlem13.o O = h T I B
10 dihmeetlem13.i I = DIsoH K W
11 dihmeetlem13.u U = DVecH K W
12 dihmeetlem13.z 0 ˙ = 0 U
13 dihmeetlem13.f F = ι h T | h P = Q
14 dihmeetlem13.g G = ι h T | h P = R
15 5 10 dihvalrel K HL W H Rel I Q
16 15 3ad2ant1 K HL W H Q A ¬ Q ˙ W R A ¬ R ˙ W Q R Rel I Q
17 relin1 Rel I Q Rel I Q I R
18 16 17 syl K HL W H Q A ¬ Q ˙ W R A ¬ R ˙ W Q R Rel I Q I R
19 elin f s I Q I R f s I Q f s I R
20 simp1 K HL W H Q A ¬ Q ˙ W R A ¬ R ˙ W Q R K HL W H
21 simp2l K HL W H Q A ¬ Q ˙ W R A ¬ R ˙ W Q R Q A ¬ Q ˙ W
22 vex f V
23 vex s V
24 2 4 5 6 7 8 10 13 22 23 dihopelvalcqat K HL W H Q A ¬ Q ˙ W f s I Q f = s F s E
25 20 21 24 syl2anc K HL W H Q A ¬ Q ˙ W R A ¬ R ˙ W Q R f s I Q f = s F s E
26 simp2r K HL W H Q A ¬ Q ˙ W R A ¬ R ˙ W Q R R A ¬ R ˙ W
27 2 4 5 6 7 8 10 14 22 23 dihopelvalcqat K HL W H R A ¬ R ˙ W f s I R f = s G s E
28 20 26 27 syl2anc K HL W H Q A ¬ Q ˙ W R A ¬ R ˙ W Q R f s I R f = s G s E
29 25 28 anbi12d K HL W H Q A ¬ Q ˙ W R A ¬ R ˙ W Q R f s I Q f s I R f = s F s E f = s G s E
30 19 29 syl5bb K HL W H Q A ¬ Q ˙ W R A ¬ R ˙ W Q R f s I Q I R f = s F s E f = s G s E
31 simprll K HL W H Q A ¬ Q ˙ W R A ¬ R ˙ W Q R f = s F s E f = s G s E f = s F
32 simpl3 K HL W H Q A ¬ Q ˙ W R A ¬ R ˙ W Q R f = s F s E f = s G s E Q R
33 fveq1 F = G F P = G P
34 simpl1 K HL W H Q A ¬ Q ˙ W R A ¬ R ˙ W Q R f = s F s E f = s G s E K HL W H
35 2 4 5 6 lhpocnel2 K HL W H P A ¬ P ˙ W
36 34 35 syl K HL W H Q A ¬ Q ˙ W R A ¬ R ˙ W Q R f = s F s E f = s G s E P A ¬ P ˙ W
37 simpl2l K HL W H Q A ¬ Q ˙ W R A ¬ R ˙ W Q R f = s F s E f = s G s E Q A ¬ Q ˙ W
38 2 4 5 7 13 ltrniotaval K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F P = Q
39 34 36 37 38 syl3anc K HL W H Q A ¬ Q ˙ W R A ¬ R ˙ W Q R f = s F s E f = s G s E F P = Q
40 simpl2r K HL W H Q A ¬ Q ˙ W R A ¬ R ˙ W Q R f = s F s E f = s G s E R A ¬ R ˙ W
41 2 4 5 7 14 ltrniotaval K HL W H P A ¬ P ˙ W R A ¬ R ˙ W G P = R
42 34 36 40 41 syl3anc K HL W H Q A ¬ Q ˙ W R A ¬ R ˙ W Q R f = s F s E f = s G s E G P = R
43 39 42 eqeq12d K HL W H Q A ¬ Q ˙ W R A ¬ R ˙ W Q R f = s F s E f = s G s E F P = G P Q = R
44 33 43 syl5ib K HL W H Q A ¬ Q ˙ W R A ¬ R ˙ W Q R f = s F s E f = s G s E F = G Q = R
45 44 necon3d K HL W H Q A ¬ Q ˙ W R A ¬ R ˙ W Q R f = s F s E f = s G s E Q R F G
46 32 45 mpd K HL W H Q A ¬ Q ˙ W R A ¬ R ˙ W Q R f = s F s E f = s G s E F G
47 simp2ll K HL W H Q A ¬ Q ˙ W R A ¬ R ˙ W Q R f = s F s E f = s G s E s O f = s F
48 simp2rl K HL W H Q A ¬ Q ˙ W R A ¬ R ˙ W Q R f = s F s E f = s G s E s O f = s G
49 47 48 eqtr3d K HL W H Q A ¬ Q ˙ W R A ¬ R ˙ W Q R f = s F s E f = s G s E s O s F = s G
50 simp11 K HL W H Q A ¬ Q ˙ W R A ¬ R ˙ W Q R f = s F s E f = s G s E s O K HL W H
51 simp2rr K HL W H Q A ¬ Q ˙ W R A ¬ R ˙ W Q R f = s F s E f = s G s E s O s E
52 simp3 K HL W H Q A ¬ Q ˙ W R A ¬ R ˙ W Q R f = s F s E f = s G s E s O s O
53 50 35 syl K HL W H Q A ¬ Q ˙ W R A ¬ R ˙ W Q R f = s F s E f = s G s E s O P A ¬ P ˙ W
54 simp12l K HL W H Q A ¬ Q ˙ W R A ¬ R ˙ W Q R f = s F s E f = s G s E s O Q A ¬ Q ˙ W
55 2 4 5 7 13 ltrniotacl K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T
56 50 53 54 55 syl3anc K HL W H Q A ¬ Q ˙ W R A ¬ R ˙ W Q R f = s F s E f = s G s E s O F T
57 simp12r K HL W H Q A ¬ Q ˙ W R A ¬ R ˙ W Q R f = s F s E f = s G s E s O R A ¬ R ˙ W
58 2 4 5 7 14 ltrniotacl K HL W H P A ¬ P ˙ W R A ¬ R ˙ W G T
59 50 53 57 58 syl3anc K HL W H Q A ¬ Q ˙ W R A ¬ R ˙ W Q R f = s F s E f = s G s E s O G T
60 1 5 7 8 9 tendospcanN K HL W H s E s O F T G T s F = s G F = G
61 50 51 52 56 59 60 syl122anc K HL W H Q A ¬ Q ˙ W R A ¬ R ˙ W Q R f = s F s E f = s G s E s O s F = s G F = G
62 49 61 mpbid K HL W H Q A ¬ Q ˙ W R A ¬ R ˙ W Q R f = s F s E f = s G s E s O F = G
63 62 3expia K HL W H Q A ¬ Q ˙ W R A ¬ R ˙ W Q R f = s F s E f = s G s E s O F = G
64 63 necon1d K HL W H Q A ¬ Q ˙ W R A ¬ R ˙ W Q R f = s F s E f = s G s E F G s = O
65 46 64 mpd K HL W H Q A ¬ Q ˙ W R A ¬ R ˙ W Q R f = s F s E f = s G s E s = O
66 65 fveq1d K HL W H Q A ¬ Q ˙ W R A ¬ R ˙ W Q R f = s F s E f = s G s E s F = O F
67 34 36 37 55 syl3anc K HL W H Q A ¬ Q ˙ W R A ¬ R ˙ W Q R f = s F s E f = s G s E F T
68 9 1 tendo02 F T O F = I B
69 67 68 syl K HL W H Q A ¬ Q ˙ W R A ¬ R ˙ W Q R f = s F s E f = s G s E O F = I B
70 31 66 69 3eqtrd K HL W H Q A ¬ Q ˙ W R A ¬ R ˙ W Q R f = s F s E f = s G s E f = I B
71 70 65 jca K HL W H Q A ¬ Q ˙ W R A ¬ R ˙ W Q R f = s F s E f = s G s E f = I B s = O
72 71 ex K HL W H Q A ¬ Q ˙ W R A ¬ R ˙ W Q R f = s F s E f = s G s E f = I B s = O
73 30 72 sylbid K HL W H Q A ¬ Q ˙ W R A ¬ R ˙ W Q R f s I Q I R f = I B s = O
74 opex f s V
75 74 elsn f s I B O f s = I B O
76 22 23 opth f s = I B O f = I B s = O
77 75 76 bitr2i f = I B s = O f s I B O
78 1 5 7 11 12 9 dvh0g K HL W H 0 ˙ = I B O
79 78 3ad2ant1 K HL W H Q A ¬ Q ˙ W R A ¬ R ˙ W Q R 0 ˙ = I B O
80 79 sneqd K HL W H Q A ¬ Q ˙ W R A ¬ R ˙ W Q R 0 ˙ = I B O
81 80 eleq2d K HL W H Q A ¬ Q ˙ W R A ¬ R ˙ W Q R f s 0 ˙ f s I B O
82 77 81 bitr4id K HL W H Q A ¬ Q ˙ W R A ¬ R ˙ W Q R f = I B s = O f s 0 ˙
83 73 82 sylibd K HL W H Q A ¬ Q ˙ W R A ¬ R ˙ W Q R f s I Q I R f s 0 ˙
84 18 83 relssdv K HL W H Q A ¬ Q ˙ W R A ¬ R ˙ W Q R I Q I R 0 ˙
85 5 11 20 dvhlmod K HL W H Q A ¬ Q ˙ W R A ¬ R ˙ W Q R U LMod
86 simp2ll K HL W H Q A ¬ Q ˙ W R A ¬ R ˙ W Q R Q A
87 1 4 atbase Q A Q B
88 86 87 syl K HL W H Q A ¬ Q ˙ W R A ¬ R ˙ W Q R Q B
89 eqid LSubSp U = LSubSp U
90 1 5 10 11 89 dihlss K HL W H Q B I Q LSubSp U
91 20 88 90 syl2anc K HL W H Q A ¬ Q ˙ W R A ¬ R ˙ W Q R I Q LSubSp U
92 simp2rl K HL W H Q A ¬ Q ˙ W R A ¬ R ˙ W Q R R A
93 1 4 atbase R A R B
94 92 93 syl K HL W H Q A ¬ Q ˙ W R A ¬ R ˙ W Q R R B
95 1 5 10 11 89 dihlss K HL W H R B I R LSubSp U
96 20 94 95 syl2anc K HL W H Q A ¬ Q ˙ W R A ¬ R ˙ W Q R I R LSubSp U
97 89 lssincl U LMod I Q LSubSp U I R LSubSp U I Q I R LSubSp U
98 85 91 96 97 syl3anc K HL W H Q A ¬ Q ˙ W R A ¬ R ˙ W Q R I Q I R LSubSp U
99 12 89 lss0ss U LMod I Q I R LSubSp U 0 ˙ I Q I R
100 85 98 99 syl2anc K HL W H Q A ¬ Q ˙ W R A ¬ R ˙ W Q R 0 ˙ I Q I R
101 84 100 eqssd K HL W H Q A ¬ Q ˙ W R A ¬ R ˙ W Q R I Q I R = 0 ˙