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