Metamath Proof Explorer

Theorem dib2dim

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

Ref Expression
Hypotheses dib2dim.l ⊢ ≤ = ( le ‘ 𝐾 )
dib2dim.j ⊢ ∨ = ( join ‘ 𝐾 )
dib2dim.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
dib2dim.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
dib2dim.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
dib2dim.s ⊢ ⊕ = ( LSSum ‘ 𝑈 )
dib2dim.i ⊢ 𝐼 = ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 )
dib2dim.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
dib2dim.p ⊢ ( 𝜑 → ( 𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊 ) )
dib2dim.q ⊢ ( 𝜑 → ( 𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊 ) )
Assertion dib2dim ( 𝜑 → ( 𝐼 ‘ ( 𝑃 ∨ 𝑄 ) ) ⊆ ( ( 𝐼 ‘ 𝑃 ) ⊕ ( 𝐼 ‘ 𝑄 ) ) )

Proof

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