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