Metamath Proof Explorer


Theorem dihopelvalcpre

Description: Member of value of isomorphism H for a lattice K when -. X .<_ W , given auxiliary atom Q . TODO: refactor to be shorter and more understandable; add lemmas? (Contributed by NM, 13-Mar-2014)

Ref Expression
Hypotheses dihopelvalcp.b B = Base K
dihopelvalcp.l ˙ = K
dihopelvalcp.j ˙ = join K
dihopelvalcp.m ˙ = meet K
dihopelvalcp.a A = Atoms K
dihopelvalcp.h H = LHyp K
dihopelvalcp.p P = oc K W
dihopelvalcp.t T = LTrn K W
dihopelvalcp.r R = trL K W
dihopelvalcp.e E = TEndo K W
dihopelvalcp.i I = DIsoH K W
dihopelvalcp.g G = ι g T | g P = Q
dihopelvalcp.f F V
dihopelvalcp.s S V
dihopelvalcp.z Z = h T I B
dihopelvalcp.n N = DIsoB K W
dihopelvalcp.c C = DIsoC K W
dihopelvalcp.u U = DVecH K W
dihopelvalcp.d + ˙ = + U
dihopelvalcp.v V = LSubSp U
dihopelvalcp.y ˙ = LSSum U
dihopelvalcp.o O = a E , b E h T a h b h
Assertion dihopelvalcpre 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

Proof

Step Hyp Ref Expression
1 dihopelvalcp.b B = Base K
2 dihopelvalcp.l ˙ = K
3 dihopelvalcp.j ˙ = join K
4 dihopelvalcp.m ˙ = meet K
5 dihopelvalcp.a A = Atoms K
6 dihopelvalcp.h H = LHyp K
7 dihopelvalcp.p P = oc K W
8 dihopelvalcp.t T = LTrn K W
9 dihopelvalcp.r R = trL K W
10 dihopelvalcp.e E = TEndo K W
11 dihopelvalcp.i I = DIsoH K W
12 dihopelvalcp.g G = ι g T | g P = Q
13 dihopelvalcp.f F V
14 dihopelvalcp.s S V
15 dihopelvalcp.z Z = h T I B
16 dihopelvalcp.n N = DIsoB K W
17 dihopelvalcp.c C = DIsoC K W
18 dihopelvalcp.u U = DVecH K W
19 dihopelvalcp.d + ˙ = + U
20 dihopelvalcp.v V = LSubSp U
21 dihopelvalcp.y ˙ = LSSum U
22 dihopelvalcp.o O = a E , b E h T a h b h
23 1 2 3 4 5 6 11 16 17 18 21 dihvalcq K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X I X = C Q ˙ N X ˙ W
24 23 eleq2d K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X F S I X F S C Q ˙ N X ˙ W
25 simp1 K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X K HL W H
26 simp3l K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X Q A ¬ Q ˙ W
27 2 5 6 18 17 20 diclss K HL W H Q A ¬ Q ˙ W C Q V
28 25 26 27 syl2anc K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X C Q V
29 simp1l K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X K HL
30 29 hllatd K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X K Lat
31 simp2l K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X X B
32 simp1r K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X W H
33 1 6 lhpbase W H W B
34 32 33 syl K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X W B
35 1 4 latmcl K Lat X B W B X ˙ W B
36 30 31 34 35 syl3anc K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X X ˙ W B
37 1 2 4 latmle2 K Lat X B W B X ˙ W ˙ W
38 30 31 34 37 syl3anc K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X X ˙ W ˙ W
39 1 2 6 18 16 20 diblss K HL W H X ˙ W B X ˙ W ˙ W N X ˙ W V
40 25 36 38 39 syl12anc K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X N X ˙ W V
41 6 18 19 20 21 dvhopellsm K HL W H C Q V N X ˙ W V F S C Q ˙ N X ˙ W x y z w x y C Q z w N X ˙ W F S = x y + ˙ z w
42 25 28 40 41 syl3anc K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X F S C Q ˙ N X ˙ W x y z w x y C Q z w N X ˙ W F S = x y + ˙ z w
43 vex x V
44 vex y V
45 2 5 6 7 8 10 17 12 43 44 dicopelval2 K HL W H Q A ¬ Q ˙ W x y C Q x = y G y E
46 25 26 45 syl2anc K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x y C Q x = y G y E
47 1 2 6 8 9 15 16 dibopelval3 K HL W H X ˙ W B X ˙ W ˙ W z w N X ˙ W z T R z ˙ X ˙ W w = Z
48 25 36 38 47 syl12anc K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X z w N X ˙ W z T R z ˙ X ˙ W w = Z
49 46 48 anbi12d K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x y C Q z w N X ˙ W x = y G y E z T R z ˙ X ˙ W w = Z
50 49 anbi1d K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x y C Q z w N X ˙ W F S = x y + ˙ z w x = y G y E z T R z ˙ X ˙ W w = Z F S = x y + ˙ z w
51 simpl1 K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = y G y E z T R z ˙ X ˙ W w = Z K HL W H
52 simprll K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = y G y E z T R z ˙ X ˙ W w = Z x = y G
53 simprlr K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = y G y E z T R z ˙ X ˙ W w = Z y E
54 2 5 6 7 lhpocnel2 K HL W H P A ¬ P ˙ W
55 51 54 syl K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = y G y E z T R z ˙ X ˙ W w = Z P A ¬ P ˙ W
56 simpl3l K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = y G y E z T R z ˙ X ˙ W w = Z Q A ¬ Q ˙ W
57 2 5 6 8 12 ltrniotacl K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W G T
58 51 55 56 57 syl3anc K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = y G y E z T R z ˙ X ˙ W w = Z G T
59 6 8 10 tendocl K HL W H y E G T y G T
60 51 53 58 59 syl3anc K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = y G y E z T R z ˙ X ˙ W w = Z y G T
61 52 60 eqeltrd K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = y G y E z T R z ˙ X ˙ W w = Z x T
62 simprll x = y G y E z T R z ˙ X ˙ W w = Z z T
63 62 adantl K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = y G y E z T R z ˙ X ˙ W w = Z z T
64 simprrr K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = y G y E z T R z ˙ X ˙ W w = Z w = Z
65 1 6 8 10 15 tendo0cl K HL W H Z E
66 51 65 syl K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = y G y E z T R z ˙ X ˙ W w = Z Z E
67 64 66 eqeltrd K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = y G y E z T R z ˙ X ˙ W w = Z w E
68 eqid Scalar U = Scalar U
69 eqid + Scalar U = + Scalar U
70 6 8 10 18 68 19 69 dvhopvadd K HL W H x T y E z T w E x y + ˙ z w = x z y + Scalar U w
71 51 61 53 63 67 70 syl122anc K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = y G y E z T R z ˙ X ˙ W w = Z x y + ˙ z w = x z y + Scalar U w
72 6 8 10 18 68 22 69 dvhfplusr K HL W H + Scalar U = O
73 51 72 syl K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = y G y E z T R z ˙ X ˙ W w = Z + Scalar U = O
74 73 oveqd K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = y G y E z T R z ˙ X ˙ W w = Z y + Scalar U w = y O w
75 74 opeq2d K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = y G y E z T R z ˙ X ˙ W w = Z x z y + Scalar U w = x z y O w
76 71 75 eqtrd K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = y G y E z T R z ˙ X ˙ W w = Z x y + ˙ z w = x z y O w
77 76 eqeq2d K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = y G y E z T R z ˙ X ˙ W w = Z F S = x y + ˙ z w F S = x z y O w
78 13 14 opth F S = x z y O w F = x z S = y O w
79 64 oveq2d K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = y G y E z T R z ˙ X ˙ W w = Z y O w = y O Z
80 1 6 8 10 15 22 tendo0plr K HL W H y E y O Z = y
81 51 53 80 syl2anc K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = y G y E z T R z ˙ X ˙ W w = Z y O Z = y
82 79 81 eqtrd K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = y G y E z T R z ˙ X ˙ W w = Z y O w = y
83 82 eqeq2d K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = y G y E z T R z ˙ X ˙ W w = Z S = y O w S = y
84 83 anbi2d K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = y G y E z T R z ˙ X ˙ W w = Z F = x z S = y O w F = x z S = y
85 78 84 syl5bb K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = y G y E z T R z ˙ X ˙ W w = Z F S = x z y O w F = x z S = y
86 77 85 bitrd K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = y G y E z T R z ˙ X ˙ W w = Z F S = x y + ˙ z w F = x z S = y
87 86 pm5.32da K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = y G y E z T R z ˙ X ˙ W w = Z F S = x y + ˙ z w x = y G y E z T R z ˙ X ˙ W w = Z F = x z S = y
88 simplll x = y G y E z T R z ˙ X ˙ W w = Z F = x z S = y x = y G
89 88 adantl K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = y G y E z T R z ˙ X ˙ W w = Z F = x z S = y x = y G
90 simprrr K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = y G y E z T R z ˙ X ˙ W w = Z F = x z S = y S = y
91 90 fveq1d K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = y G y E z T R z ˙ X ˙ W w = Z F = x z S = y S G = y G
92 89 91 eqtr4d K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = y G y E z T R z ˙ X ˙ W w = Z F = x z S = y x = S G
93 90 eqcomd K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = y G y E z T R z ˙ X ˙ W w = Z F = x z S = y y = S
94 coass S G -1 S G z = S G -1 S G z
95 simpl1 K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = y G y E z T R z ˙ X ˙ W w = Z F = x z S = y K HL W H
96 simpllr x = y G y E z T R z ˙ X ˙ W w = Z F = x z S = y y E
97 96 adantl K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = y G y E z T R z ˙ X ˙ W w = Z F = x z S = y y E
98 90 97 eqeltrd K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = y G y E z T R z ˙ X ˙ W w = Z F = x z S = y S E
99 58 adantrr K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = y G y E z T R z ˙ X ˙ W w = Z F = x z S = y G T
100 6 8 10 tendocl K HL W H S E G T S G T
101 95 98 99 100 syl3anc K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = y G y E z T R z ˙ X ˙ W w = Z F = x z S = y S G T
102 1 6 8 ltrn1o K HL W H S G T S G : B 1-1 onto B
103 95 101 102 syl2anc K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = y G y E z T R z ˙ X ˙ W w = Z F = x z S = y S G : B 1-1 onto B
104 f1ococnv1 S G : B 1-1 onto B S G -1 S G = I B
105 103 104 syl K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = y G y E z T R z ˙ X ˙ W w = Z F = x z S = y S G -1 S G = I B
106 105 coeq1d K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = y G y E z T R z ˙ X ˙ W w = Z F = x z S = y S G -1 S G z = I B z
107 62 ad2antrl K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = y G y E z T R z ˙ X ˙ W w = Z F = x z S = y z T
108 1 6 8 ltrn1o K HL W H z T z : B 1-1 onto B
109 95 107 108 syl2anc K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = y G y E z T R z ˙ X ˙ W w = Z F = x z S = y z : B 1-1 onto B
110 f1of z : B 1-1 onto B z : B B
111 fcoi2 z : B B I B z = z
112 109 110 111 3syl K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = y G y E z T R z ˙ X ˙ W w = Z F = x z S = y I B z = z
113 106 112 eqtr2d K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = y G y E z T R z ˙ X ˙ W w = Z F = x z S = y z = S G -1 S G z
114 simprrl K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = y G y E z T R z ˙ X ˙ W w = Z F = x z S = y F = x z
115 92 coeq1d K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = y G y E z T R z ˙ X ˙ W w = Z F = x z S = y x z = S G z
116 114 115 eqtrd K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = y G y E z T R z ˙ X ˙ W w = Z F = x z S = y F = S G z
117 116 coeq1d K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = y G y E z T R z ˙ X ˙ W w = Z F = x z S = y F S G -1 = S G z S G -1
118 6 8 ltrncnv K HL W H S G T S G -1 T
119 95 101 118 syl2anc K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = y G y E z T R z ˙ X ˙ W w = Z F = x z S = y S G -1 T
120 6 8 ltrnco K HL W H S G T z T S G z T
121 95 101 107 120 syl3anc K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = y G y E z T R z ˙ X ˙ W w = Z F = x z S = y S G z T
122 6 8 ltrncom K HL W H S G -1 T S G z T S G -1 S G z = S G z S G -1
123 95 119 121 122 syl3anc K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = y G y E z T R z ˙ X ˙ W w = Z F = x z S = y S G -1 S G z = S G z S G -1
124 117 123 eqtr4d K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = y G y E z T R z ˙ X ˙ W w = Z F = x z S = y F S G -1 = S G -1 S G z
125 94 113 124 3eqtr4a K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = y G y E z T R z ˙ X ˙ W w = Z F = x z S = y z = F S G -1
126 simplrr x = y G y E z T R z ˙ X ˙ W w = Z F = x z S = y w = Z
127 126 adantl K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = y G y E z T R z ˙ X ˙ W w = Z F = x z S = y w = Z
128 125 127 jca K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = y G y E z T R z ˙ X ˙ W w = Z F = x z S = y z = F S G -1 w = Z
129 92 93 128 jca31 K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = y G y E z T R z ˙ X ˙ W w = Z F = x z S = y x = S G y = S z = F S G -1 w = Z
130 129 ex K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = y G y E z T R z ˙ X ˙ W w = Z F = x z S = y x = S G y = S z = F S G -1 w = Z
131 130 pm4.71rd K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = y G y E z T R z ˙ X ˙ W w = Z F = x z S = y x = S G y = S z = F S G -1 w = Z x = y G y E z T R z ˙ X ˙ W w = Z F = x z S = y
132 87 131 bitrd K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = y G y E z T R z ˙ X ˙ W w = Z F S = x y + ˙ z w x = S G y = S z = F S G -1 w = Z x = y G y E z T R z ˙ X ˙ W w = Z F = x z S = y
133 simprrl K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = S G y = S z = F S G -1 w = Z x = y G y E z T R z ˙ X ˙ W w = Z F = x z S = y F = x z
134 simpll1 K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = S G y = S z = F S G -1 w = Z x = y G y E z T R z ˙ X ˙ W w = Z F = x z S = y K HL W H
135 88 adantl K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = S G y = S z = F S G -1 w = Z x = y G y E z T R z ˙ X ˙ W w = Z F = x z S = y x = y G
136 96 adantl K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = S G y = S z = F S G -1 w = Z x = y G y E z T R z ˙ X ˙ W w = Z F = x z S = y y E
137 134 54 syl K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = S G y = S z = F S G -1 w = Z x = y G y E z T R z ˙ X ˙ W w = Z F = x z S = y P A ¬ P ˙ W
138 simpl3l K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = S G y = S z = F S G -1 w = Z Q A ¬ Q ˙ W
139 138 adantr K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = S G y = S z = F S G -1 w = Z x = y G y E z T R z ˙ X ˙ W w = Z F = x z S = y Q A ¬ Q ˙ W
140 134 137 139 57 syl3anc K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = S G y = S z = F S G -1 w = Z x = y G y E z T R z ˙ X ˙ W w = Z F = x z S = y G T
141 134 136 140 59 syl3anc K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = S G y = S z = F S G -1 w = Z x = y G y E z T R z ˙ X ˙ W w = Z F = x z S = y y G T
142 135 141 eqeltrd K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = S G y = S z = F S G -1 w = Z x = y G y E z T R z ˙ X ˙ W w = Z F = x z S = y x T
143 62 ad2antrl K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = S G y = S z = F S G -1 w = Z x = y G y E z T R z ˙ X ˙ W w = Z F = x z S = y z T
144 6 8 ltrnco K HL W H x T z T x z T
145 134 142 143 144 syl3anc K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = S G y = S z = F S G -1 w = Z x = y G y E z T R z ˙ X ˙ W w = Z F = x z S = y x z T
146 133 145 eqeltrd K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = S G y = S z = F S G -1 w = Z x = y G y E z T R z ˙ X ˙ W w = Z F = x z S = y F T
147 simpl1l K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = S G y = S z = F S G -1 w = Z K HL
148 147 adantr K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = S G y = S z = F S G -1 w = Z x = y G y E z T R z ˙ X ˙ W w = Z F = x z S = y K HL
149 148 hllatd K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = S G y = S z = F S G -1 w = Z x = y G y E z T R z ˙ X ˙ W w = Z F = x z S = y K Lat
150 1 6 8 9 trlcl K HL W H z T R z B
151 134 143 150 syl2anc K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = S G y = S z = F S G -1 w = Z x = y G y E z T R z ˙ X ˙ W w = Z F = x z S = y R z B
152 simpl2l K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = S G y = S z = F S G -1 w = Z X B
153 152 adantr K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = S G y = S z = F S G -1 w = Z x = y G y E z T R z ˙ X ˙ W w = Z F = x z S = y X B
154 simpl1r K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = S G y = S z = F S G -1 w = Z W H
155 154 adantr K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = S G y = S z = F S G -1 w = Z x = y G y E z T R z ˙ X ˙ W w = Z F = x z S = y W H
156 155 33 syl K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = S G y = S z = F S G -1 w = Z x = y G y E z T R z ˙ X ˙ W w = Z F = x z S = y W B
157 149 153 156 35 syl3anc K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = S G y = S z = F S G -1 w = Z x = y G y E z T R z ˙ X ˙ W w = Z F = x z S = y X ˙ W B
158 simprlr x = y G y E z T R z ˙ X ˙ W w = Z R z ˙ X ˙ W
159 158 ad2antrl K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = S G y = S z = F S G -1 w = Z x = y G y E z T R z ˙ X ˙ W w = Z F = x z S = y R z ˙ X ˙ W
160 1 2 4 latmle1 K Lat X B W B X ˙ W ˙ X
161 149 153 156 160 syl3anc K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = S G y = S z = F S G -1 w = Z x = y G y E z T R z ˙ X ˙ W w = Z F = x z S = y X ˙ W ˙ X
162 1 2 149 151 157 153 159 161 lattrd K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = S G y = S z = F S G -1 w = Z x = y G y E z T R z ˙ X ˙ W w = Z F = x z S = y R z ˙ X
163 146 136 162 jca31 K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = S G y = S z = F S G -1 w = Z x = y G y E z T R z ˙ X ˙ W w = Z F = x z S = y F T y E R z ˙ X
164 simprll K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = S G y = S z = F S G -1 w = Z x = S G
165 164 adantr K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = S G y = S z = F S G -1 w = Z F T y E R z ˙ X x = S G
166 simprlr K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = S G y = S z = F S G -1 w = Z y = S
167 166 adantr K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = S G y = S z = F S G -1 w = Z F T y E R z ˙ X y = S
168 167 fveq1d K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = S G y = S z = F S G -1 w = Z F T y E R z ˙ X y G = S G
169 165 168 eqtr4d K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = S G y = S z = F S G -1 w = Z F T y E R z ˙ X x = y G
170 simprlr K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = S G y = S z = F S G -1 w = Z F T y E R z ˙ X y E
171 169 170 jca K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = S G y = S z = F S G -1 w = Z F T y E R z ˙ X x = y G y E
172 simprrl K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = S G y = S z = F S G -1 w = Z z = F S G -1
173 172 adantr K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = S G y = S z = F S G -1 w = Z F T y E R z ˙ X z = F S G -1
174 simpll1 K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = S G y = S z = F S G -1 w = Z F T y E R z ˙ X K HL W H
175 simprll K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = S G y = S z = F S G -1 w = Z F T y E R z ˙ X F T
176 167 170 eqeltrrd K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = S G y = S z = F S G -1 w = Z F T y E R z ˙ X S E
177 174 54 syl K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = S G y = S z = F S G -1 w = Z F T y E R z ˙ X P A ¬ P ˙ W
178 138 adantr K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = S G y = S z = F S G -1 w = Z F T y E R z ˙ X Q A ¬ Q ˙ W
179 174 177 178 57 syl3anc K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = S G y = S z = F S G -1 w = Z F T y E R z ˙ X G T
180 174 176 179 100 syl3anc K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = S G y = S z = F S G -1 w = Z F T y E R z ˙ X S G T
181 174 180 118 syl2anc K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = S G y = S z = F S G -1 w = Z F T y E R z ˙ X S G -1 T
182 6 8 ltrnco K HL W H F T S G -1 T F S G -1 T
183 174 175 181 182 syl3anc K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = S G y = S z = F S G -1 w = Z F T y E R z ˙ X F S G -1 T
184 173 183 eqeltrd K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = S G y = S z = F S G -1 w = Z F T y E R z ˙ X z T
185 simprr K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = S G y = S z = F S G -1 w = Z F T y E R z ˙ X R z ˙ X
186 2 6 8 9 trlle K HL W H z T R z ˙ W
187 174 184 186 syl2anc K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = S G y = S z = F S G -1 w = Z F T y E R z ˙ X R z ˙ W
188 147 adantr K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = S G y = S z = F S G -1 w = Z F T y E R z ˙ X K HL
189 188 hllatd K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = S G y = S z = F S G -1 w = Z F T y E R z ˙ X K Lat
190 174 184 150 syl2anc K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = S G y = S z = F S G -1 w = Z F T y E R z ˙ X R z B
191 152 adantr K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = S G y = S z = F S G -1 w = Z F T y E R z ˙ X X B
192 154 adantr K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = S G y = S z = F S G -1 w = Z F T y E R z ˙ X W H
193 192 33 syl K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = S G y = S z = F S G -1 w = Z F T y E R z ˙ X W B
194 1 2 4 latlem12 K Lat R z B X B W B R z ˙ X R z ˙ W R z ˙ X ˙ W
195 189 190 191 193 194 syl13anc K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = S G y = S z = F S G -1 w = Z F T y E R z ˙ X R z ˙ X R z ˙ W R z ˙ X ˙ W
196 185 187 195 mpbi2and K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = S G y = S z = F S G -1 w = Z F T y E R z ˙ X R z ˙ X ˙ W
197 simprrr K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = S G y = S z = F S G -1 w = Z w = Z
198 197 adantr K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = S G y = S z = F S G -1 w = Z F T y E R z ˙ X w = Z
199 184 196 198 jca31 K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = S G y = S z = F S G -1 w = Z F T y E R z ˙ X z T R z ˙ X ˙ W w = Z
200 174 180 102 syl2anc K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = S G y = S z = F S G -1 w = Z F T y E R z ˙ X S G : B 1-1 onto B
201 200 104 syl K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = S G y = S z = F S G -1 w = Z F T y E R z ˙ X S G -1 S G = I B
202 201 coeq2d K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = S G y = S z = F S G -1 w = Z F T y E R z ˙ X F S G -1 S G = F I B
203 1 6 8 ltrn1o K HL W H F T F : B 1-1 onto B
204 174 175 203 syl2anc K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = S G y = S z = F S G -1 w = Z F T y E R z ˙ X F : B 1-1 onto B
205 f1of F : B 1-1 onto B F : B B
206 fcoi1 F : B B F I B = F
207 204 205 206 3syl K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = S G y = S z = F S G -1 w = Z F T y E R z ˙ X F I B = F
208 202 207 eqtr2d K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = S G y = S z = F S G -1 w = Z F T y E R z ˙ X F = F S G -1 S G
209 coass F S G -1 S G = F S G -1 S G
210 208 209 syl6eqr K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = S G y = S z = F S G -1 w = Z F T y E R z ˙ X F = F S G -1 S G
211 6 8 ltrncom K HL W H S G T F S G -1 T S G F S G -1 = F S G -1 S G
212 174 180 183 211 syl3anc K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = S G y = S z = F S G -1 w = Z F T y E R z ˙ X S G F S G -1 = F S G -1 S G
213 210 212 eqtr4d K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = S G y = S z = F S G -1 w = Z F T y E R z ˙ X F = S G F S G -1
214 165 173 coeq12d K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = S G y = S z = F S G -1 w = Z F T y E R z ˙ X x z = S G F S G -1
215 213 214 eqtr4d K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = S G y = S z = F S G -1 w = Z F T y E R z ˙ X F = x z
216 167 eqcomd K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = S G y = S z = F S G -1 w = Z F T y E R z ˙ X S = y
217 215 216 jca K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = S G y = S z = F S G -1 w = Z F T y E R z ˙ X F = x z S = y
218 171 199 217 jca31 K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = S G y = S z = F S G -1 w = Z F T y E R z ˙ X x = y G y E z T R z ˙ X ˙ W w = Z F = x z S = y
219 163 218 impbida K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = S G y = S z = F S G -1 w = Z x = y G y E z T R z ˙ X ˙ W w = Z F = x z S = y F T y E R z ˙ X
220 219 pm5.32da K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = S G y = S z = F S G -1 w = Z x = y G y E z T R z ˙ X ˙ W w = Z F = x z S = y x = S G y = S z = F S G -1 w = Z F T y E R z ˙ X
221 df-3an x = S G y = S z = F S G -1 w = Z F T y E R z ˙ X x = S G y = S z = F S G -1 w = Z F T y E R z ˙ X
222 220 221 syl6bbr K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x = S G y = S z = F S G -1 w = Z x = y G y E z T R z ˙ X ˙ W w = Z F = x z S = y x = S G y = S z = F S G -1 w = Z F T y E R z ˙ X
223 50 132 222 3bitrd K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x y C Q z w N X ˙ W F S = x y + ˙ z w x = S G y = S z = F S G -1 w = Z F T y E R z ˙ X
224 223 4exbidv K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x y z w x y C Q z w N X ˙ W F S = x y + ˙ z w x y z w x = S G y = S z = F S G -1 w = Z F T y E R z ˙ X
225 fvex S G V
226 225 cnvex S G -1 V
227 13 226 coex F S G -1 V
228 8 fvexi T V
229 228 mptex h T I B V
230 15 229 eqeltri Z V
231 biidd x = S G F T y E R z ˙ X F T y E R z ˙ X
232 eleq1 y = S y E S E
233 232 anbi2d y = S F T y E F T S E
234 233 anbi1d y = S F T y E R z ˙ X F T S E R z ˙ X
235 fveq2 z = F S G -1 R z = R F S G -1
236 235 breq1d z = F S G -1 R z ˙ X R F S G -1 ˙ X
237 236 anbi2d z = F S G -1 F T S E R z ˙ X F T S E R F S G -1 ˙ X
238 biidd w = Z F T S E R F S G -1 ˙ X F T S E R F S G -1 ˙ X
239 225 14 227 230 231 234 237 238 ceqsex4v x y z w x = S G y = S z = F S G -1 w = Z F T y E R z ˙ X F T S E R F S G -1 ˙ X
240 224 239 syl6bb K HL W H X B ¬ X ˙ W Q A ¬ Q ˙ W Q ˙ X ˙ W = X x y z w x y C Q z w N X ˙ W F S = x y + ˙ z w F T S E R F S G -1 ˙ X
241 24 42 240 3bitrd 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