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

Metamath Proof Explorer

Theorem dihjatb

Description: Isomorphism H of lattice join of two atoms under the fiducial hyperplane. (Contributed by NM, 23-Sep-2014)

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

Proof

Step Hyp Ref Expression
1 dihjatb.l ⊢ ≤ = ( le ‘ 𝐾 )
2 dihjatb.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
3 dihjatb.j ⊢ ∨ = ( join ‘ 𝐾 )
4 dihjatb.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
5 dihjatb.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
6 dihjatb.s ⊢ ⊕ = ( LSSum ‘ 𝑈 )
7 dihjatb.i ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
8 dihjatb.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
9 dihjatb.p ⊢ ( 𝜑 → ( 𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊 ) )
10 dihjatb.q ⊢ ( 𝜑 → ( 𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊 ) )
11 1 3 4 2 5 6 7 8 9 10 dih2dimb ⊢ ( 𝜑 → ( 𝐼 ‘ ( 𝑃 ∨ 𝑄 ) ) ⊆ ( ( 𝐼 ‘ 𝑃 ) ⊕ ( 𝐼 ‘ 𝑄 ) ) )
12 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
13 9 simpld ⊢ ( 𝜑 → 𝑃 ∈ 𝐴 )
14 12 4 atbase ⊢ ( 𝑃 ∈ 𝐴 → 𝑃 ∈ ( Base ‘ 𝐾 ) )
15 13 14 syl ⊢ ( 𝜑 → 𝑃 ∈ ( Base ‘ 𝐾 ) )
16 10 simpld ⊢ ( 𝜑 → 𝑄 ∈ 𝐴 )
17 12 4 atbase ⊢ ( 𝑄 ∈ 𝐴 → 𝑄 ∈ ( Base ‘ 𝐾 ) )
18 16 17 syl ⊢ ( 𝜑 → 𝑄 ∈ ( Base ‘ 𝐾 ) )
19 12 2 3 5 6 7 8 15 18 dihsumssj ⊢ ( 𝜑 → ( ( 𝐼 ‘ 𝑃 ) ⊕ ( 𝐼 ‘ 𝑄 ) ) ⊆ ( 𝐼 ‘ ( 𝑃 ∨ 𝑄 ) ) )
20 11 19 eqssd ⊢ ( 𝜑 → ( 𝐼 ‘ ( 𝑃 ∨ 𝑄 ) ) = ( ( 𝐼 ‘ 𝑃 ) ⊕ ( 𝐼 ‘ 𝑄 ) ) )