Metamath Proof Explorer


Theorem dih2dimbALTN

Description: Extend dia2dim to isomorphism H. (This version combines dib2dim and dih2dimb for shorter overall proof, but may be less easy to understand. TODO: decide which to use.) (Contributed by NM, 22-Sep-2014) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses dih2dimb.l ˙ = K
dih2dimb.j ˙ = join K
dih2dimb.a A = Atoms K
dih2dimb.h H = LHyp K
dih2dimb.u U = DVecH K W
dih2dimb.s ˙ = LSSum U
dih2dimb.i I = DIsoH K W
dih2dimb.k φ K HL W H
dih2dimb.p φ P A P ˙ W
dih2dimb.q φ Q A Q ˙ W
Assertion dih2dimbALTN φ I P ˙ Q I P ˙ I Q

Proof

Step Hyp Ref Expression
1 dih2dimb.l ˙ = K
2 dih2dimb.j ˙ = join K
3 dih2dimb.a A = Atoms K
4 dih2dimb.h H = LHyp K
5 dih2dimb.u U = DVecH K W
6 dih2dimb.s ˙ = LSSum U
7 dih2dimb.i I = DIsoH K W
8 dih2dimb.k φ K HL W H
9 dih2dimb.p φ P A P ˙ W
10 dih2dimb.q φ Q A Q ˙ W
11 eqid DIsoB K W = DIsoB K W
12 4 11 dibvalrel K HL W H Rel DIsoB K W P ˙ Q
13 8 12 syl φ Rel DIsoB K W P ˙ Q
14 eqid DVecA K W = DVecA K W
15 eqid LSSum DVecA K W = LSSum DVecA K W
16 eqid DIsoA K W = DIsoA K W
17 1 2 3 4 14 15 16 8 9 10 dia2dim φ DIsoA K W P ˙ Q DIsoA K W P LSSum DVecA K W DIsoA K W Q
18 17 sseld φ f DIsoA K W P ˙ Q f DIsoA K W P LSSum DVecA K W DIsoA K W Q
19 18 anim1d φ f DIsoA K W P ˙ Q s = f LTrn K W I Base K f DIsoA K W P LSSum DVecA K W DIsoA K W Q s = f LTrn K W I Base K
20 8 simpld φ K HL
21 9 simpld φ P A
22 10 simpld φ Q A
23 eqid Base K = Base K
24 23 2 3 hlatjcl K HL P A Q A P ˙ Q Base K
25 20 21 22 24 syl3anc φ P ˙ Q Base K
26 9 simprd φ P ˙ W
27 10 simprd φ Q ˙ W
28 hllat K HL K Lat
29 20 28 syl φ K Lat
30 23 3 atbase P A P Base K
31 21 30 syl φ P Base K
32 23 3 atbase Q A Q Base K
33 22 32 syl φ Q Base K
34 8 simprd φ W H
35 23 4 lhpbase W H W Base K
36 34 35 syl φ W Base K
37 23 1 2 latjle12 K Lat P Base K Q Base K W Base K P ˙ W Q ˙ W P ˙ Q ˙ W
38 29 31 33 36 37 syl13anc φ P ˙ W Q ˙ W P ˙ Q ˙ W
39 26 27 38 mpbi2and φ P ˙ Q ˙ W
40 eqid LTrn K W = LTrn K W
41 eqid f LTrn K W I Base K = f LTrn K W I Base K
42 23 1 4 40 41 16 11 dibopelval2 K HL W H P ˙ Q Base K P ˙ Q ˙ W f s DIsoB K W P ˙ Q f DIsoA K W P ˙ Q s = f LTrn K W I Base K
43 8 25 39 42 syl12anc φ f s DIsoB K W P ˙ Q f DIsoA K W P ˙ Q s = f LTrn K W I Base K
44 31 26 jca φ P Base K P ˙ W
45 33 27 jca φ Q Base K Q ˙ W
46 23 1 4 40 41 14 5 15 6 16 11 8 44 45 diblsmopel φ f s DIsoB K W P ˙ DIsoB K W Q f DIsoA K W P LSSum DVecA K W DIsoA K W Q s = f LTrn K W I Base K
47 19 43 46 3imtr4d φ f s DIsoB K W P ˙ Q f s DIsoB K W P ˙ DIsoB K W Q
48 13 47 relssdv φ DIsoB K W P ˙ Q DIsoB K W P ˙ DIsoB K W Q
49 23 1 4 7 11 dihvalb K HL W H P ˙ Q Base K P ˙ Q ˙ W I P ˙ Q = DIsoB K W P ˙ Q
50 8 25 39 49 syl12anc φ I P ˙ Q = DIsoB K W P ˙ Q
51 23 1 4 7 11 dihvalb K HL W H P Base K P ˙ W I P = DIsoB K W P
52 8 31 26 51 syl12anc φ I P = DIsoB K W P
53 23 1 4 7 11 dihvalb K HL W H Q Base K Q ˙ W I Q = DIsoB K W Q
54 8 33 27 53 syl12anc φ I Q = DIsoB K W Q
55 52 54 oveq12d φ I P ˙ I Q = DIsoB K W P ˙ DIsoB K W Q
56 48 50 55 3sstr4d φ I P ˙ Q I P ˙ I Q