Metamath Proof Explorer


Theorem dihjatc1

Description: Lemma for isomorphism H of a lattice meet. TODO: shorter proof if we change .\/ order of ( X ./\ Y ) .\/ Q here and down? (Contributed by NM, 6-Apr-2014)

Ref Expression
Hypotheses dihjatc1.b B = Base K
dihjatc1.l ˙ = K
dihjatc1.h H = LHyp K
dihjatc1.j ˙ = join K
dihjatc1.m ˙ = meet K
dihjatc1.a A = Atoms K
dihjatc1.u U = DVecH K W
dihjatc1.s ˙ = LSSum U
dihjatc1.i I = DIsoH K W
Assertion dihjatc1 K HL W H X B Y B Q A ¬ Q ˙ W Q ˙ X X ˙ Y ˙ W I X ˙ Y ˙ Q = I Q ˙ I X ˙ Y

Proof

Step Hyp Ref Expression
1 dihjatc1.b B = Base K
2 dihjatc1.l ˙ = K
3 dihjatc1.h H = LHyp K
4 dihjatc1.j ˙ = join K
5 dihjatc1.m ˙ = meet K
6 dihjatc1.a A = Atoms K
7 dihjatc1.u U = DVecH K W
8 dihjatc1.s ˙ = LSSum U
9 dihjatc1.i I = DIsoH K W
10 simp11 K HL W H X B Y B Q A ¬ Q ˙ W Q ˙ X X ˙ Y ˙ W K HL W H
11 simp11l K HL W H X B Y B Q A ¬ Q ˙ W Q ˙ X X ˙ Y ˙ W K HL
12 11 hllatd K HL W H X B Y B Q A ¬ Q ˙ W Q ˙ X X ˙ Y ˙ W K Lat
13 simp12 K HL W H X B Y B Q A ¬ Q ˙ W Q ˙ X X ˙ Y ˙ W X B
14 simp13 K HL W H X B Y B Q A ¬ Q ˙ W Q ˙ X X ˙ Y ˙ W Y B
15 1 5 latmcl K Lat X B Y B X ˙ Y B
16 12 13 14 15 syl3anc K HL W H X B Y B Q A ¬ Q ˙ W Q ˙ X X ˙ Y ˙ W X ˙ Y B
17 simp2l K HL W H X B Y B Q A ¬ Q ˙ W Q ˙ X X ˙ Y ˙ W Q A
18 1 6 atbase Q A Q B
19 17 18 syl K HL W H X B Y B Q A ¬ Q ˙ W Q ˙ X X ˙ Y ˙ W Q B
20 1 4 latjcl K Lat X ˙ Y B Q B X ˙ Y ˙ Q B
21 12 16 19 20 syl3anc K HL W H X B Y B Q A ¬ Q ˙ W Q ˙ X X ˙ Y ˙ W X ˙ Y ˙ Q B
22 simp2 K HL W H X B Y B Q A ¬ Q ˙ W Q ˙ X X ˙ Y ˙ W Q A ¬ Q ˙ W
23 simp3l K HL W H X B Y B Q A ¬ Q ˙ W Q ˙ X X ˙ Y ˙ W Q ˙ X
24 1 2 3 4 5 6 dihmeetlem6 K HL W H X B Y B Q A ¬ Q ˙ W Q ˙ X ¬ X ˙ Y ˙ Q ˙ W
25 10 13 14 22 23 24 syl32anc K HL W H X B Y B Q A ¬ Q ˙ W Q ˙ X X ˙ Y ˙ W ¬ X ˙ Y ˙ Q ˙ W
26 1 2 4 5 6 dihmeetlem5 K HL X B Y B Q A Q ˙ X X ˙ Y ˙ Q = X ˙ Y ˙ Q
27 11 13 14 17 23 26 syl32anc K HL W H X B Y B Q A ¬ Q ˙ W Q ˙ X X ˙ Y ˙ W X ˙ Y ˙ Q = X ˙ Y ˙ Q
28 27 breq1d K HL W H X B Y B Q A ¬ Q ˙ W Q ˙ X X ˙ Y ˙ W X ˙ Y ˙ Q ˙ W X ˙ Y ˙ Q ˙ W
29 25 28 mtbid K HL W H X B Y B Q A ¬ Q ˙ W Q ˙ X X ˙ Y ˙ W ¬ X ˙ Y ˙ Q ˙ W
30 1 2 4 latlej2 K Lat X ˙ Y B Q B Q ˙ X ˙ Y ˙ Q
31 12 16 19 30 syl3anc K HL W H X B Y B Q A ¬ Q ˙ W Q ˙ X X ˙ Y ˙ W Q ˙ X ˙ Y ˙ Q
32 1 2 4 5 6 3 9 7 8 dihvalcq2 K HL W H X ˙ Y ˙ Q B ¬ X ˙ Y ˙ Q ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ Y ˙ Q I X ˙ Y ˙ Q = I Q ˙ I X ˙ Y ˙ Q ˙ W
33 10 21 29 22 31 32 syl122anc K HL W H X B Y B Q A ¬ Q ˙ W Q ˙ X X ˙ Y ˙ W I X ˙ Y ˙ Q = I Q ˙ I X ˙ Y ˙ Q ˙ W
34 eqid 0. K = 0. K
35 2 5 34 6 3 lhpmat K HL W H Q A ¬ Q ˙ W Q ˙ W = 0. K
36 10 22 35 syl2anc K HL W H X B Y B Q A ¬ Q ˙ W Q ˙ X X ˙ Y ˙ W Q ˙ W = 0. K
37 36 oveq2d K HL W H X B Y B Q A ¬ Q ˙ W Q ˙ X X ˙ Y ˙ W X ˙ Y ˙ Q ˙ W = X ˙ Y ˙ 0. K
38 simp11r K HL W H X B Y B Q A ¬ Q ˙ W Q ˙ X X ˙ Y ˙ W W H
39 1 3 lhpbase W H W B
40 38 39 syl K HL W H X B Y B Q A ¬ Q ˙ W Q ˙ X X ˙ Y ˙ W W B
41 simp3r K HL W H X B Y B Q A ¬ Q ˙ W Q ˙ X X ˙ Y ˙ W X ˙ Y ˙ W
42 1 2 4 5 6 atmod1i2 K HL Q A X ˙ Y B W B X ˙ Y ˙ W X ˙ Y ˙ Q ˙ W = X ˙ Y ˙ Q ˙ W
43 11 17 16 40 41 42 syl131anc K HL W H X B Y B Q A ¬ Q ˙ W Q ˙ X X ˙ Y ˙ W X ˙ Y ˙ Q ˙ W = X ˙ Y ˙ Q ˙ W
44 hlol K HL K OL
45 11 44 syl K HL W H X B Y B Q A ¬ Q ˙ W Q ˙ X X ˙ Y ˙ W K OL
46 1 4 34 olj01 K OL X ˙ Y B X ˙ Y ˙ 0. K = X ˙ Y
47 45 16 46 syl2anc K HL W H X B Y B Q A ¬ Q ˙ W Q ˙ X X ˙ Y ˙ W X ˙ Y ˙ 0. K = X ˙ Y
48 37 43 47 3eqtr3d K HL W H X B Y B Q A ¬ Q ˙ W Q ˙ X X ˙ Y ˙ W X ˙ Y ˙ Q ˙ W = X ˙ Y
49 48 fveq2d K HL W H X B Y B Q A ¬ Q ˙ W Q ˙ X X ˙ Y ˙ W I X ˙ Y ˙ Q ˙ W = I X ˙ Y
50 49 oveq2d K HL W H X B Y B Q A ¬ Q ˙ W Q ˙ X X ˙ Y ˙ W I Q ˙ I X ˙ Y ˙ Q ˙ W = I Q ˙ I X ˙ Y
51 33 50 eqtrd K HL W H X B Y B Q A ¬ Q ˙ W Q ˙ X X ˙ Y ˙ W I X ˙ Y ˙ Q = I Q ˙ I X ˙ Y