Metamath Proof Explorer

Theorem dib2dim

Description: Extend dia2dim to partial isomorphism B. (Contributed by NM, 22-Sep-2014)

Ref Expression
Hypotheses dib2dim.l ⊢ ≤ ˙ = ≤ K
dib2dim.j ⊢ ∨ ˙ = join ⁡ K
dib2dim.a ⊢ A = Atoms ⁡ K
dib2dim.h ⊢ H = LHyp ⁡ K
dib2dim.u ⊢ U = DVecH ⁡ K ⁡ W
dib2dim.s ⊢ ⊕ ˙ = LSSum ⁡ U
dib2dim.i ⊢ I = DIsoB ⁡ K ⁡ W
dib2dim.k ⊢ φ → K ∈ HL ∧ W ∈ H
dib2dim.p ⊢ φ → P ∈ A ∧ P ≤ ˙ W
dib2dim.q ⊢ φ → Q ∈ A ∧ Q ≤ ˙ W
Assertion dib2dim ⊢ φ → I ⁡ P ∨ ˙ Q ⊆ I ⁡ P ⊕ ˙ I ⁡ Q

Proof

Step Hyp Ref Expression
1 dib2dim.l ⊢ ≤ ˙ = ≤ K
2 dib2dim.j ⊢ ∨ ˙ = join ⁡ K
3 dib2dim.a ⊢ A = Atoms ⁡ K
4 dib2dim.h ⊢ H = LHyp ⁡ K
5 dib2dim.u ⊢ U = DVecH ⁡ K ⁡ W
6 dib2dim.s ⊢ ⊕ ˙ = LSSum ⁡ U
7 dib2dim.i ⊢ I = DIsoB ⁡ K ⁡ W
8 dib2dim.k ⊢ φ → K ∈ HL ∧ W ∈ H
9 dib2dim.p ⊢ φ → P ∈ A ∧ P ≤ ˙ W
10 dib2dim.q ⊢ φ → Q ∈ A ∧ Q ≤ ˙ W
11 4 7 dibvalrel ⊢ K ∈ HL ∧ W ∈ H → Rel ⁡ I ⁡ P ∨ ˙ Q
12 8 11 syl ⊢ φ → Rel ⁡ I ⁡ P ∨ ˙ Q
13 eqid ⊢ DVecA ⁡ K ⁡ W = DVecA ⁡ K ⁡ W
14 eqid ⊢ LSSum ⁡ DVecA ⁡ K ⁡ W = LSSum ⁡ DVecA ⁡ K ⁡ W
15 eqid ⊢ DIsoA ⁡ K ⁡ W = DIsoA ⁡ K ⁡ W
16 1 2 3 4 13 14 15 8 9 10 dia2dim ⊢ φ → DIsoA ⁡ K ⁡ W ⁡ P ∨ ˙ Q ⊆ DIsoA ⁡ K ⁡ W ⁡ P LSSum ⁡ DVecA ⁡ K ⁡ W DIsoA ⁡ K ⁡ W ⁡ Q
17 16 sseld ⊢ φ → f ∈ DIsoA ⁡ K ⁡ W ⁡ P ∨ ˙ Q → f ∈ DIsoA ⁡ K ⁡ W ⁡ P LSSum ⁡ DVecA ⁡ K ⁡ W DIsoA ⁡ K ⁡ W ⁡ Q
18 17 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
19 8 simpld ⊢ φ → K ∈ HL
20 9 simpld ⊢ φ → P ∈ A
21 10 simpld ⊢ φ → Q ∈ A
22 eqid ⊢ Base K = Base K
23 22 2 3 hlatjcl ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A → P ∨ ˙ Q ∈ Base K
24 19 20 21 23 syl3anc ⊢ φ → P ∨ ˙ Q ∈ Base K
25 9 simprd ⊢ φ → P ≤ ˙ W
26 10 simprd ⊢ φ → Q ≤ ˙ W
27 19 hllatd ⊢ φ → K ∈ Lat
28 22 3 atbase ⊢ P ∈ A → P ∈ Base K
29 20 28 syl ⊢ φ → P ∈ Base K
30 22 3 atbase ⊢ Q ∈ A → Q ∈ Base K
31 21 30 syl ⊢ φ → Q ∈ Base K
32 8 simprd ⊢ φ → W ∈ H
33 22 4 lhpbase ⊢ W ∈ H → W ∈ Base K
34 32 33 syl ⊢ φ → W ∈ Base K
35 22 1 2 latjle12 ⊢ K ∈ Lat ∧ P ∈ Base K ∧ Q ∈ Base K ∧ W ∈ Base K → P ≤ ˙ W ∧ Q ≤ ˙ W ↔ P ∨ ˙ Q ≤ ˙ W
36 27 29 31 34 35 syl13anc ⊢ φ → P ≤ ˙ W ∧ Q ≤ ˙ W ↔ P ∨ ˙ Q ≤ ˙ W
37 25 26 36 mpbi2and ⊢ φ → P ∨ ˙ Q ≤ ˙ W
38 eqid ⊢ LTrn ⁡ K ⁡ W = LTrn ⁡ K ⁡ W
39 eqid ⊢ f ∈ LTrn ⁡ K ⁡ W ⟼ I ↾ Base K = f ∈ LTrn ⁡ K ⁡ W ⟼ I ↾ Base K
40 22 1 4 38 39 15 7 dibopelval2 ⊢ K ∈ HL ∧ W ∈ H ∧ P ∨ ˙ Q ∈ Base K ∧ P ∨ ˙ Q ≤ ˙ W → f s ∈ I ⁡ P ∨ ˙ Q ↔ f ∈ DIsoA ⁡ K ⁡ W ⁡ P ∨ ˙ Q ∧ s = f ∈ LTrn ⁡ K ⁡ W ⟼ I ↾ Base K
41 8 24 37 40 syl12anc ⊢ φ → f s ∈ I ⁡ P ∨ ˙ Q ↔ f ∈ DIsoA ⁡ K ⁡ W ⁡ P ∨ ˙ Q ∧ s = f ∈ LTrn ⁡ K ⁡ W ⟼ I ↾ Base K
42 29 25 jca ⊢ φ → P ∈ Base K ∧ P ≤ ˙ W
43 31 26 jca ⊢ φ → Q ∈ Base K ∧ Q ≤ ˙ W
44 22 1 4 38 39 13 5 14 6 15 7 8 42 43 diblsmopel ⊢ φ → f s ∈ I ⁡ P ⊕ ˙ I ⁡ Q ↔ f ∈ DIsoA ⁡ K ⁡ W ⁡ P LSSum ⁡ DVecA ⁡ K ⁡ W DIsoA ⁡ K ⁡ W ⁡ Q ∧ s = f ∈ LTrn ⁡ K ⁡ W ⟼ I ↾ Base K
45 18 41 44 3imtr4d ⊢ φ → f s ∈ I ⁡ P ∨ ˙ Q → f s ∈ I ⁡ P ⊕ ˙ I ⁡ Q
46 12 45 relssdv ⊢ φ → I ⁡ P ∨ ˙ Q ⊆ I ⁡ P ⊕ ˙ I ⁡ Q