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 ⊢ ≤ = ( le ‘ 𝐾 )
dih2dimb.j ⊢ ∨ = ( join ‘ 𝐾 )
dih2dimb.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
dih2dimb.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
dih2dimb.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
dih2dimb.s ⊢ ⊕ = ( LSSum ‘ 𝑈 )
dih2dimb.i ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
dih2dimb.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
dih2dimb.p ⊢ ( 𝜑 → ( 𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊 ) )
dih2dimb.q ⊢ ( 𝜑 → ( 𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊 ) )
Assertion dih2dimbALTN ( 𝜑 → ( 𝐼 ‘ ( 𝑃 ∨ 𝑄 ) ) ⊆ ( ( 𝐼 ‘ 𝑃 ) ⊕ ( 𝐼 ‘ 𝑄 ) ) )

Proof

Step Hyp Ref Expression
1 dih2dimb.l ⊢ ≤ = ( le ‘ 𝐾 )
2 dih2dimb.j ⊢ ∨ = ( join ‘ 𝐾 )
3 dih2dimb.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4 dih2dimb.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
5 dih2dimb.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
6 dih2dimb.s ⊢ ⊕ = ( LSSum ‘ 𝑈 )
7 dih2dimb.i ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
8 dih2dimb.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
9 dih2dimb.p ⊢ ( 𝜑 → ( 𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊 ) )
10 dih2dimb.q ⊢ ( 𝜑 → ( 𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊 ) )
11 eqid ⊢ ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) = ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 )
12 4 11 dibvalrel ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → Rel ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑃 ∨ 𝑄 ) ) )
13 8 12 syl ⊢ ( 𝜑 → Rel ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑃 ∨ 𝑄 ) ) )
14 eqid ⊢ ( ( DVecA ‘ 𝐾 ) ‘ 𝑊 ) = ( ( DVecA ‘ 𝐾 ) ‘ 𝑊 )
15 eqid ⊢ ( LSSum ‘ ( ( DVecA ‘ 𝐾 ) ‘ 𝑊 ) ) = ( LSSum ‘ ( ( DVecA ‘ 𝐾 ) ‘ 𝑊 ) )
16 eqid ⊢ ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) = ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 )
17 1 2 3 4 14 15 16 8 9 10 dia2dim ⊢ ( 𝜑 → ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑃 ∨ 𝑄 ) ) ⊆ ( ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑃 ) ( LSSum ‘ ( ( DVecA ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑄 ) ) )
18 17 sseld ⊢ ( 𝜑 → ( 𝑓 ∈ ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑃 ∨ 𝑄 ) ) → 𝑓 ∈ ( ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑃 ) ( LSSum ‘ ( ( DVecA ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑄 ) ) ) )
19 18 anim1d ⊢ ( 𝜑 → ( ( 𝑓 ∈ ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑃 ∨ 𝑄 ) ) ∧ 𝑠 = ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) ) → ( 𝑓 ∈ ( ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑃 ) ( LSSum ‘ ( ( DVecA ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑄 ) ) ∧ 𝑠 = ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) ) ) )
20 8 simpld ⊢ ( 𝜑 → 𝐾 ∈ HL )
21 9 simpld ⊢ ( 𝜑 → 𝑃 ∈ 𝐴 )
22 10 simpld ⊢ ( 𝜑 → 𝑄 ∈ 𝐴 )
23 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
24 23 2 3 hlatjcl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
25 20 21 22 24 syl3anc ⊢ ( 𝜑 → ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
26 9 simprd ⊢ ( 𝜑 → 𝑃 ≤ 𝑊 )
27 10 simprd ⊢ ( 𝜑 → 𝑄 ≤ 𝑊 )
28 hllat ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ Lat )
29 20 28 syl ⊢ ( 𝜑 → 𝐾 ∈ Lat )
30 23 3 atbase ⊢ ( 𝑃 ∈ 𝐴 → 𝑃 ∈ ( Base ‘ 𝐾 ) )
31 21 30 syl ⊢ ( 𝜑 → 𝑃 ∈ ( Base ‘ 𝐾 ) )
32 23 3 atbase ⊢ ( 𝑄 ∈ 𝐴 → 𝑄 ∈ ( Base ‘ 𝐾 ) )
33 22 32 syl ⊢ ( 𝜑 → 𝑄 ∈ ( Base ‘ 𝐾 ) )
34 8 simprd ⊢ ( 𝜑 → 𝑊 ∈ 𝐻 )
35 23 4 lhpbase ⊢ ( 𝑊 ∈ 𝐻 → 𝑊 ∈ ( Base ‘ 𝐾 ) )
36 34 35 syl ⊢ ( 𝜑 → 𝑊 ∈ ( Base ‘ 𝐾 ) )
37 23 1 2 latjle12 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ 𝑄 ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑃 ≤ 𝑊 ∧ 𝑄 ≤ 𝑊 ) ↔ ( 𝑃 ∨ 𝑄 ) ≤ 𝑊 ) )
38 29 31 33 36 37 syl13anc ⊢ ( 𝜑 → ( ( 𝑃 ≤ 𝑊 ∧ 𝑄 ≤ 𝑊 ) ↔ ( 𝑃 ∨ 𝑄 ) ≤ 𝑊 ) )
39 26 27 38 mpbi2and ⊢ ( 𝜑 → ( 𝑃 ∨ 𝑄 ) ≤ 𝑊 )
40 eqid ⊢ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
41 eqid ⊢ ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) = ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ ( Base ‘ 𝐾 ) ) )
42 23 1 4 40 41 16 11 dibopelval2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑃 ∨ 𝑄 ) ≤ 𝑊 ) ) → ( ⟨ 𝑓 , 𝑠 ⟩ ∈ ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑃 ∨ 𝑄 ) ) ↔ ( 𝑓 ∈ ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑃 ∨ 𝑄 ) ) ∧ 𝑠 = ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) ) ) )
43 8 25 39 42 syl12anc ⊢ ( 𝜑 → ( ⟨ 𝑓 , 𝑠 ⟩ ∈ ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑃 ∨ 𝑄 ) ) ↔ ( 𝑓 ∈ ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑃 ∨ 𝑄 ) ) ∧ 𝑠 = ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) ) ) )
44 31 26 jca ⊢ ( 𝜑 → ( 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ 𝑃 ≤ 𝑊 ) )
45 33 27 jca ⊢ ( 𝜑 → ( 𝑄 ∈ ( Base ‘ 𝐾 ) ∧ 𝑄 ≤ 𝑊 ) )
46 23 1 4 40 41 14 5 15 6 16 11 8 44 45 diblsmopel ⊢ ( 𝜑 → ( ⟨ 𝑓 , 𝑠 ⟩ ∈ ( ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑃 ) ⊕ ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑄 ) ) ↔ ( 𝑓 ∈ ( ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑃 ) ( LSSum ‘ ( ( DVecA ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑄 ) ) ∧ 𝑠 = ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) ) ) )
47 19 43 46 3imtr4d ⊢ ( 𝜑 → ( ⟨ 𝑓 , 𝑠 ⟩ ∈ ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑃 ∨ 𝑄 ) ) → ⟨ 𝑓 , 𝑠 ⟩ ∈ ( ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑃 ) ⊕ ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑄 ) ) ) )
48 13 47 relssdv ⊢ ( 𝜑 → ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑃 ∨ 𝑄 ) ) ⊆ ( ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑃 ) ⊕ ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑄 ) ) )
49 23 1 4 7 11 dihvalb ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑃 ∨ 𝑄 ) ≤ 𝑊 ) ) → ( 𝐼 ‘ ( 𝑃 ∨ 𝑄 ) ) = ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑃 ∨ 𝑄 ) ) )
50 8 25 39 49 syl12anc ⊢ ( 𝜑 → ( 𝐼 ‘ ( 𝑃 ∨ 𝑄 ) ) = ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑃 ∨ 𝑄 ) ) )
51 23 1 4 7 11 dihvalb ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ 𝑃 ≤ 𝑊 ) ) → ( 𝐼 ‘ 𝑃 ) = ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑃 ) )
52 8 31 26 51 syl12anc ⊢ ( 𝜑 → ( 𝐼 ‘ 𝑃 ) = ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑃 ) )
53 23 1 4 7 11 dihvalb ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ ( Base ‘ 𝐾 ) ∧ 𝑄 ≤ 𝑊 ) ) → ( 𝐼 ‘ 𝑄 ) = ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑄 ) )
54 8 33 27 53 syl12anc ⊢ ( 𝜑 → ( 𝐼 ‘ 𝑄 ) = ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑄 ) )
55 52 54 oveq12d ⊢ ( 𝜑 → ( ( 𝐼 ‘ 𝑃 ) ⊕ ( 𝐼 ‘ 𝑄 ) ) = ( ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑃 ) ⊕ ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑄 ) ) )
56 48 50 55 3sstr4d ⊢ ( 𝜑 → ( 𝐼 ‘ ( 𝑃 ∨ 𝑄 ) ) ⊆ ( ( 𝐼 ‘ 𝑃 ) ⊕ ( 𝐼 ‘ 𝑄 ) ) )