dihjat3

Description: Isomorphism H of lattice join with an atom. (Contributed by NM, 25-Apr-2015)

	Ref	Expression
Hypotheses	dihjat3.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	dihjat3.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	dihjat3.j	⊢ ∨ = ( join ‘ 𝐾 )
	dihjat3.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
	dihjat3.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	dihjat3.s	⊢ ⊕ = ( LSSum ‘ 𝑈 )
	dihjat3.i	⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
	dihjat3.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
	dihjat3.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	dihjat3.p	⊢ ( 𝜑 → 𝑃 ∈ 𝐴 )
Assertion	dihjat3	⊢ ( 𝜑 → ( 𝐼 ‘ ( 𝑋 ∨ 𝑃 ) ) = ( ( 𝐼 ‘ 𝑋 ) ⊕ ( 𝐼 ‘ 𝑃 ) ) )

Proof

Step	Hyp	Ref	Expression
1		dihjat3.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		dihjat3.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
3		dihjat3.j	⊢ ∨ = ( join ‘ 𝐾 )
4		dihjat3.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
5		dihjat3.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
6		dihjat3.s	⊢ ⊕ = ( LSSum ‘ 𝑈 )
7		dihjat3.i	⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
8		dihjat3.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
9		dihjat3.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
10		dihjat3.p	⊢ ( 𝜑 → 𝑃 ∈ 𝐴 )
11	1 4	atbase	⊢ ( 𝑃 ∈ 𝐴 → 𝑃 ∈ 𝐵 )
12	10 11	syl	⊢ ( 𝜑 → 𝑃 ∈ 𝐵 )
13		eqid	⊢ ( ( joinH ‘ 𝐾 ) ‘ 𝑊 ) = ( ( joinH ‘ 𝐾 ) ‘ 𝑊 )
14	1 3 2 7 13	djhlj	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐵 ) ) → ( 𝐼 ‘ ( 𝑋 ∨ 𝑃 ) ) = ( ( 𝐼 ‘ 𝑋 ) ( ( joinH ‘ 𝐾 ) ‘ 𝑊 ) ( 𝐼 ‘ 𝑃 ) ) )
15	8 9 12 14	syl12anc	⊢ ( 𝜑 → ( 𝐼 ‘ ( 𝑋 ∨ 𝑃 ) ) = ( ( 𝐼 ‘ 𝑋 ) ( ( joinH ‘ 𝐾 ) ‘ 𝑊 ) ( 𝐼 ‘ 𝑃 ) ) )
16		eqid	⊢ ( LSAtoms ‘ 𝑈 ) = ( LSAtoms ‘ 𝑈 )
17	1 2 7	dihcl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ) → ( 𝐼 ‘ 𝑋 ) ∈ ran 𝐼 )
18	8 9 17	syl2anc	⊢ ( 𝜑 → ( 𝐼 ‘ 𝑋 ) ∈ ran 𝐼 )
19	4 2 5 7 16	dihatlat	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑃 ∈ 𝐴 ) → ( 𝐼 ‘ 𝑃 ) ∈ ( LSAtoms ‘ 𝑈 ) )
20	8 10 19	syl2anc	⊢ ( 𝜑 → ( 𝐼 ‘ 𝑃 ) ∈ ( LSAtoms ‘ 𝑈 ) )
21	2 7 13 5 6 16 8 18 20	dihjat2	⊢ ( 𝜑 → ( ( 𝐼 ‘ 𝑋 ) ( ( joinH ‘ 𝐾 ) ‘ 𝑊 ) ( 𝐼 ‘ 𝑃 ) ) = ( ( 𝐼 ‘ 𝑋 ) ⊕ ( 𝐼 ‘ 𝑃 ) ) )
22	15 21	eqtrd	⊢ ( 𝜑 → ( 𝐼 ‘ ( 𝑋 ∨ 𝑃 ) ) = ( ( 𝐼 ‘ 𝑋 ) ⊕ ( 𝐼 ‘ 𝑃 ) ) )

Metamath Proof Explorer

Theorem dihjat3

Proof