This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dih2dimb

Description: Extend dib2dim to isomorphism H. (Contributed by NM, 22-Sep-2014)

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 dih2dimb ( 𝜑 → ( 𝐼 ‘ ( 𝑃 ∨ 𝑄 ) ) ⊆ ( ( 𝐼 ‘ 𝑃 ) ⊕ ( 𝐼 ‘ 𝑄 ) ) )

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 1 2 3 4 5 6 11 8 9 10 dib2dim ⊢ ( 𝜑 → ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑃 ∨ 𝑄 ) ) ⊆ ( ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑃 ) ⊕ ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑄 ) ) )
13 8 simpld ⊢ ( 𝜑 → 𝐾 ∈ HL )
14 9 simpld ⊢ ( 𝜑 → 𝑃 ∈ 𝐴 )
15 10 simpld ⊢ ( 𝜑 → 𝑄 ∈ 𝐴 )
16 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
17 16 2 3 hlatjcl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
18 13 14 15 17 syl3anc ⊢ ( 𝜑 → ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
19 9 simprd ⊢ ( 𝜑 → 𝑃 ≤ 𝑊 )
20 10 simprd ⊢ ( 𝜑 → 𝑄 ≤ 𝑊 )
21 13 hllatd ⊢ ( 𝜑 → 𝐾 ∈ Lat )
22 16 3 atbase ⊢ ( 𝑃 ∈ 𝐴 → 𝑃 ∈ ( Base ‘ 𝐾 ) )
23 14 22 syl ⊢ ( 𝜑 → 𝑃 ∈ ( Base ‘ 𝐾 ) )
24 16 3 atbase ⊢ ( 𝑄 ∈ 𝐴 → 𝑄 ∈ ( Base ‘ 𝐾 ) )
25 15 24 syl ⊢ ( 𝜑 → 𝑄 ∈ ( Base ‘ 𝐾 ) )
26 8 simprd ⊢ ( 𝜑 → 𝑊 ∈ 𝐻 )
27 16 4 lhpbase ⊢ ( 𝑊 ∈ 𝐻 → 𝑊 ∈ ( Base ‘ 𝐾 ) )
28 26 27 syl ⊢ ( 𝜑 → 𝑊 ∈ ( Base ‘ 𝐾 ) )
29 16 1 2 latjle12 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ 𝑄 ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑃 ≤ 𝑊 ∧ 𝑄 ≤ 𝑊 ) ↔ ( 𝑃 ∨ 𝑄 ) ≤ 𝑊 ) )
30 21 23 25 28 29 syl13anc ⊢ ( 𝜑 → ( ( 𝑃 ≤ 𝑊 ∧ 𝑄 ≤ 𝑊 ) ↔ ( 𝑃 ∨ 𝑄 ) ≤ 𝑊 ) )
31 19 20 30 mpbi2and ⊢ ( 𝜑 → ( 𝑃 ∨ 𝑄 ) ≤ 𝑊 )
32 16 1 4 7 11 dihvalb ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑃 ∨ 𝑄 ) ≤ 𝑊 ) ) → ( 𝐼 ‘ ( 𝑃 ∨ 𝑄 ) ) = ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑃 ∨ 𝑄 ) ) )
33 8 18 31 32 syl12anc ⊢ ( 𝜑 → ( 𝐼 ‘ ( 𝑃 ∨ 𝑄 ) ) = ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑃 ∨ 𝑄 ) ) )
34 16 1 4 7 11 dihvalb ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ 𝑃 ≤ 𝑊 ) ) → ( 𝐼 ‘ 𝑃 ) = ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑃 ) )
35 8 23 19 34 syl12anc ⊢ ( 𝜑 → ( 𝐼 ‘ 𝑃 ) = ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑃 ) )
36 16 1 4 7 11 dihvalb ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ ( Base ‘ 𝐾 ) ∧ 𝑄 ≤ 𝑊 ) ) → ( 𝐼 ‘ 𝑄 ) = ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑄 ) )
37 8 25 20 36 syl12anc ⊢ ( 𝜑 → ( 𝐼 ‘ 𝑄 ) = ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑄 ) )
38 35 37 oveq12d ⊢ ( 𝜑 → ( ( 𝐼 ‘ 𝑃 ) ⊕ ( 𝐼 ‘ 𝑄 ) ) = ( ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑃 ) ⊕ ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑄 ) ) )
39 12 33 38 3sstr4d ⊢ ( 𝜑 → ( 𝐼 ‘ ( 𝑃 ∨ 𝑄 ) ) ⊆ ( ( 𝐼 ‘ 𝑃 ) ⊕ ( 𝐼 ‘ 𝑄 ) ) )