Metamath Proof Explorer


Theorem dihglblem5apreN

Description: A conjunction property of isomorphism H. TODO: reduce antecedent size; general review for shorter proof. (Contributed by NM, 21-Mar-2014) (New usage is discouraged.)

Ref Expression
Hypotheses dihglblem5a.b B = Base K
dihglblem5a.m ˙ = meet K
dihglblem5a.h H = LHyp K
dihglblem5a.i I = DIsoH K W
dihglblem5a.l ˙ = K
dihglblem5a.j ˙ = join K
dihglblem5a.a A = Atoms K
dihglblem5a.p P = oc K W
dihglblem5a.t T = LTrn K W
dihglblem5a.r R = trL K W
dihglblem5a.e E = TEndo K W
dihglblem5a.g G = ι h T | h P = q
dihglblem5a.o 0 ˙ = h T I B
Assertion dihglblem5apreN K HL W H X B ¬ X ˙ W I X ˙ W = I X I W

Proof

Step Hyp Ref Expression
1 dihglblem5a.b B = Base K
2 dihglblem5a.m ˙ = meet K
3 dihglblem5a.h H = LHyp K
4 dihglblem5a.i I = DIsoH K W
5 dihglblem5a.l ˙ = K
6 dihglblem5a.j ˙ = join K
7 dihglblem5a.a A = Atoms K
8 dihglblem5a.p P = oc K W
9 dihglblem5a.t T = LTrn K W
10 dihglblem5a.r R = trL K W
11 dihglblem5a.e E = TEndo K W
12 dihglblem5a.g G = ι h T | h P = q
13 dihglblem5a.o 0 ˙ = h T I B
14 hllat K HL K Lat
15 14 ad2antrr K HL W H X B ¬ X ˙ W K Lat
16 simprl K HL W H X B ¬ X ˙ W X B
17 1 3 lhpbase W H W B
18 17 ad2antlr K HL W H X B ¬ X ˙ W W B
19 1 5 2 latmle1 K Lat X B W B X ˙ W ˙ X
20 15 16 18 19 syl3anc K HL W H X B ¬ X ˙ W X ˙ W ˙ X
21 simpl K HL W H X B ¬ X ˙ W K HL W H
22 1 2 latmcl K Lat X B W B X ˙ W B
23 15 16 18 22 syl3anc K HL W H X B ¬ X ˙ W X ˙ W B
24 1 5 3 4 dihord K HL W H X ˙ W B X B I X ˙ W I X X ˙ W ˙ X
25 21 23 16 24 syl3anc K HL W H X B ¬ X ˙ W I X ˙ W I X X ˙ W ˙ X
26 20 25 mpbird K HL W H X B ¬ X ˙ W I X ˙ W I X
27 1 5 2 latmle2 K Lat X B W B X ˙ W ˙ W
28 15 16 18 27 syl3anc K HL W H X B ¬ X ˙ W X ˙ W ˙ W
29 1 5 3 4 dihord K HL W H X ˙ W B W B I X ˙ W I W X ˙ W ˙ W
30 21 23 18 29 syl3anc K HL W H X B ¬ X ˙ W I X ˙ W I W X ˙ W ˙ W
31 28 30 mpbird K HL W H X B ¬ X ˙ W I X ˙ W I W
32 26 31 ssind K HL W H X B ¬ X ˙ W I X ˙ W I X I W
33 3 4 dihvalrel K HL W H Rel I X
34 relin1 Rel I X Rel I X I W
35 33 34 syl K HL W H Rel I X I W
36 35 adantr K HL W H X B ¬ X ˙ W Rel I X I W
37 elin f s I X I W f s I X f s I W
38 1 5 6 2 7 3 lhpmcvr2 K HL W H X B ¬ X ˙ W q A ¬ q ˙ W q ˙ X ˙ W = X
39 vex f V
40 vex s V
41 1 5 6 2 7 3 8 9 10 11 4 12 39 40 dihopelvalc K HL W H X B ¬ X ˙ W q A ¬ q ˙ W q ˙ X ˙ W = X f s I X f T s E R f s G -1 ˙ X
42 id K HL W H K HL W H
43 17 adantl K HL W H W B
44 1 5 latref K Lat W B W ˙ W
45 14 17 44 syl2an K HL W H W ˙ W
46 1 5 3 9 10 13 4 dihopelvalbN K HL W H W B W ˙ W f s I W f T R f ˙ W s = 0 ˙
47 42 43 45 46 syl12anc K HL W H f s I W f T R f ˙ W s = 0 ˙
48 47 3ad2ant1 K HL W H X B ¬ X ˙ W q A ¬ q ˙ W q ˙ X ˙ W = X f s I W f T R f ˙ W s = 0 ˙
49 41 48 anbi12d K HL W H X B ¬ X ˙ W q A ¬ q ˙ W q ˙ X ˙ W = X f s I X f s I W f T s E R f s G -1 ˙ X f T R f ˙ W s = 0 ˙
50 simprll f T s E R f s G -1 ˙ X f T R f ˙ W s = 0 ˙ f T
51 50 adantl K HL W H X B ¬ X ˙ W q A ¬ q ˙ W q ˙ X ˙ W = X f T s E R f s G -1 ˙ X f T R f ˙ W s = 0 ˙ f T
52 simprrr K HL W H X B ¬ X ˙ W q A ¬ q ˙ W q ˙ X ˙ W = X f T s E R f s G -1 ˙ X f T R f ˙ W s = 0 ˙ s = 0 ˙
53 52 fveq1d K HL W H X B ¬ X ˙ W q A ¬ q ˙ W q ˙ X ˙ W = X f T s E R f s G -1 ˙ X f T R f ˙ W s = 0 ˙ s G = 0 ˙ G
54 simpl1 K HL W H X B ¬ X ˙ W q A ¬ q ˙ W q ˙ X ˙ W = X f T s E R f s G -1 ˙ X f T R f ˙ W s = 0 ˙ K HL W H
55 5 7 3 8 lhpocnel2 K HL W H P A ¬ P ˙ W
56 54 55 syl K HL W H X B ¬ X ˙ W q A ¬ q ˙ W q ˙ X ˙ W = X f T s E R f s G -1 ˙ X f T R f ˙ W s = 0 ˙ P A ¬ P ˙ W
57 simpl3l K HL W H X B ¬ X ˙ W q A ¬ q ˙ W q ˙ X ˙ W = X f T s E R f s G -1 ˙ X f T R f ˙ W s = 0 ˙ q A ¬ q ˙ W
58 5 7 3 9 12 ltrniotacl K HL W H P A ¬ P ˙ W q A ¬ q ˙ W G T
59 54 56 57 58 syl3anc K HL W H X B ¬ X ˙ W q A ¬ q ˙ W q ˙ X ˙ W = X f T s E R f s G -1 ˙ X f T R f ˙ W s = 0 ˙ G T
60 13 1 tendo02 G T 0 ˙ G = I B
61 59 60 syl K HL W H X B ¬ X ˙ W q A ¬ q ˙ W q ˙ X ˙ W = X f T s E R f s G -1 ˙ X f T R f ˙ W s = 0 ˙ 0 ˙ G = I B
62 53 61 eqtrd K HL W H X B ¬ X ˙ W q A ¬ q ˙ W q ˙ X ˙ W = X f T s E R f s G -1 ˙ X f T R f ˙ W s = 0 ˙ s G = I B
63 62 cnveqd K HL W H X B ¬ X ˙ W q A ¬ q ˙ W q ˙ X ˙ W = X f T s E R f s G -1 ˙ X f T R f ˙ W s = 0 ˙ s G -1 = I B -1
64 cnvresid I B -1 = I B
65 63 64 eqtrdi K HL W H X B ¬ X ˙ W q A ¬ q ˙ W q ˙ X ˙ W = X f T s E R f s G -1 ˙ X f T R f ˙ W s = 0 ˙ s G -1 = I B
66 65 coeq2d K HL W H X B ¬ X ˙ W q A ¬ q ˙ W q ˙ X ˙ W = X f T s E R f s G -1 ˙ X f T R f ˙ W s = 0 ˙ f s G -1 = f I B
67 1 3 9 ltrn1o K HL W H f T f : B 1-1 onto B
68 54 51 67 syl2anc K HL W H X B ¬ X ˙ W q A ¬ q ˙ W q ˙ X ˙ W = X f T s E R f s G -1 ˙ X f T R f ˙ W s = 0 ˙ f : B 1-1 onto B
69 f1of f : B 1-1 onto B f : B B
70 fcoi1 f : B B f I B = f
71 68 69 70 3syl K HL W H X B ¬ X ˙ W q A ¬ q ˙ W q ˙ X ˙ W = X f T s E R f s G -1 ˙ X f T R f ˙ W s = 0 ˙ f I B = f
72 66 71 eqtrd K HL W H X B ¬ X ˙ W q A ¬ q ˙ W q ˙ X ˙ W = X f T s E R f s G -1 ˙ X f T R f ˙ W s = 0 ˙ f s G -1 = f
73 72 fveq2d K HL W H X B ¬ X ˙ W q A ¬ q ˙ W q ˙ X ˙ W = X f T s E R f s G -1 ˙ X f T R f ˙ W s = 0 ˙ R f s G -1 = R f
74 simprlr K HL W H X B ¬ X ˙ W q A ¬ q ˙ W q ˙ X ˙ W = X f T s E R f s G -1 ˙ X f T R f ˙ W s = 0 ˙ R f s G -1 ˙ X
75 73 74 eqbrtrrd K HL W H X B ¬ X ˙ W q A ¬ q ˙ W q ˙ X ˙ W = X f T s E R f s G -1 ˙ X f T R f ˙ W s = 0 ˙ R f ˙ X
76 5 3 9 10 trlle K HL W H f T R f ˙ W
77 54 51 76 syl2anc K HL W H X B ¬ X ˙ W q A ¬ q ˙ W q ˙ X ˙ W = X f T s E R f s G -1 ˙ X f T R f ˙ W s = 0 ˙ R f ˙ W
78 simpl1l K HL W H X B ¬ X ˙ W q A ¬ q ˙ W q ˙ X ˙ W = X f T s E R f s G -1 ˙ X f T R f ˙ W s = 0 ˙ K HL
79 78 hllatd K HL W H X B ¬ X ˙ W q A ¬ q ˙ W q ˙ X ˙ W = X f T s E R f s G -1 ˙ X f T R f ˙ W s = 0 ˙ K Lat
80 1 3 9 10 trlcl K HL W H f T R f B
81 54 51 80 syl2anc K HL W H X B ¬ X ˙ W q A ¬ q ˙ W q ˙ X ˙ W = X f T s E R f s G -1 ˙ X f T R f ˙ W s = 0 ˙ R f B
82 simpl2l K HL W H X B ¬ X ˙ W q A ¬ q ˙ W q ˙ X ˙ W = X f T s E R f s G -1 ˙ X f T R f ˙ W s = 0 ˙ X B
83 simpl1r K HL W H X B ¬ X ˙ W q A ¬ q ˙ W q ˙ X ˙ W = X f T s E R f s G -1 ˙ X f T R f ˙ W s = 0 ˙ W H
84 83 17 syl K HL W H X B ¬ X ˙ W q A ¬ q ˙ W q ˙ X ˙ W = X f T s E R f s G -1 ˙ X f T R f ˙ W s = 0 ˙ W B
85 1 5 2 latlem12 K Lat R f B X B W B R f ˙ X R f ˙ W R f ˙ X ˙ W
86 79 81 82 84 85 syl13anc K HL W H X B ¬ X ˙ W q A ¬ q ˙ W q ˙ X ˙ W = X f T s E R f s G -1 ˙ X f T R f ˙ W s = 0 ˙ R f ˙ X R f ˙ W R f ˙ X ˙ W
87 75 77 86 mpbi2and K HL W H X B ¬ X ˙ W q A ¬ q ˙ W q ˙ X ˙ W = X f T s E R f s G -1 ˙ X f T R f ˙ W s = 0 ˙ R f ˙ X ˙ W
88 51 87 jca K HL W H X B ¬ X ˙ W q A ¬ q ˙ W q ˙ X ˙ W = X f T s E R f s G -1 ˙ X f T R f ˙ W s = 0 ˙ f T R f ˙ X ˙ W
89 79 82 84 22 syl3anc K HL W H X B ¬ X ˙ W q A ¬ q ˙ W q ˙ X ˙ W = X f T s E R f s G -1 ˙ X f T R f ˙ W s = 0 ˙ X ˙ W B
90 79 82 84 27 syl3anc K HL W H X B ¬ X ˙ W q A ¬ q ˙ W q ˙ X ˙ W = X f T s E R f s G -1 ˙ X f T R f ˙ W s = 0 ˙ X ˙ W ˙ W
91 1 5 3 9 10 13 4 dihopelvalbN K HL W H X ˙ W B X ˙ W ˙ W f s I X ˙ W f T R f ˙ X ˙ W s = 0 ˙
92 54 89 90 91 syl12anc K HL W H X B ¬ X ˙ W q A ¬ q ˙ W q ˙ X ˙ W = X f T s E R f s G -1 ˙ X f T R f ˙ W s = 0 ˙ f s I X ˙ W f T R f ˙ X ˙ W s = 0 ˙
93 88 52 92 mpbir2and K HL W H X B ¬ X ˙ W q A ¬ q ˙ W q ˙ X ˙ W = X f T s E R f s G -1 ˙ X f T R f ˙ W s = 0 ˙ f s I X ˙ W
94 93 ex K HL W H X B ¬ X ˙ W q A ¬ q ˙ W q ˙ X ˙ W = X f T s E R f s G -1 ˙ X f T R f ˙ W s = 0 ˙ f s I X ˙ W
95 49 94 sylbid K HL W H X B ¬ X ˙ W q A ¬ q ˙ W q ˙ X ˙ W = X f s I X f s I W f s I X ˙ W
96 95 3expia K HL W H X B ¬ X ˙ W q A ¬ q ˙ W q ˙ X ˙ W = X f s I X f s I W f s I X ˙ W
97 96 exp4c K HL W H X B ¬ X ˙ W q A ¬ q ˙ W q ˙ X ˙ W = X f s I X f s I W f s I X ˙ W
98 97 imp4a K HL W H X B ¬ X ˙ W q A ¬ q ˙ W q ˙ X ˙ W = X f s I X f s I W f s I X ˙ W
99 98 rexlimdv K HL W H X B ¬ X ˙ W q A ¬ q ˙ W q ˙ X ˙ W = X f s I X f s I W f s I X ˙ W
100 38 99 mpd K HL W H X B ¬ X ˙ W f s I X f s I W f s I X ˙ W
101 37 100 syl5bi K HL W H X B ¬ X ˙ W f s I X I W f s I X ˙ W
102 36 101 relssdv K HL W H X B ¬ X ˙ W I X I W I X ˙ W
103 32 102 eqssd K HL W H X B ¬ X ˙ W I X ˙ W = I X I W