Theorem dihjat2

Description: The subspace sum of a closed subspace and an atom is the same as their subspace join. (Contributed by NM, 1-Oct-2014)

	Ref	Expression
Hypotheses	dihjat2.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	dihjat2.i	⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
	dihjat2.j	⊢ ∨ = ( ( joinH ‘ 𝐾 ) ‘ 𝑊 )
	dihjat2.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	dihjat2.p	⊢ ⊕ = ( LSSum ‘ 𝑈 )
	dihjat2.a	⊢ 𝐴 = ( LSAtoms ‘ 𝑈 )
	dihjat2.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
	dihjat2.x	⊢ ( 𝜑 → 𝑋 ∈ ran 𝐼 )
	dihjat2.q	⊢ ( 𝜑 → 𝑄 ∈ 𝐴 )
Assertion	dihjat2	⊢ ( 𝜑 → ( 𝑋 ∨ 𝑄 ) = ( 𝑋 ⊕ 𝑄 ) )

Proof

Step	Hyp	Ref	Expression
1		dihjat2.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		dihjat2.i	⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
3		dihjat2.j	⊢ ∨ = ( ( joinH ‘ 𝐾 ) ‘ 𝑊 )
4		dihjat2.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
5		dihjat2.p	⊢ ⊕ = ( LSSum ‘ 𝑈 )
6		dihjat2.a	⊢ 𝐴 = ( LSAtoms ‘ 𝑈 )
7		dihjat2.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
8		dihjat2.x	⊢ ( 𝜑 → 𝑋 ∈ ran 𝐼 )
9		dihjat2.q	⊢ ( 𝜑 → 𝑄 ∈ 𝐴 )
10		eqid	⊢ ( Base ‘ 𝑈 ) = ( Base ‘ 𝑈 )
11		eqid	⊢ ( LSpan ‘ 𝑈 ) = ( LSpan ‘ 𝑈 )
12	7	adantr	⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( Base ‘ 𝑈 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
13	8	adantr	⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( Base ‘ 𝑈 ) ) → 𝑋 ∈ ran 𝐼 )
14		simpr	⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( Base ‘ 𝑈 ) ) → 𝑣 ∈ ( Base ‘ 𝑈 ) )
15	1 4 10 5 11 2 3 12 13 14	dihjat1	⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( Base ‘ 𝑈 ) ) → ( 𝑋 ∨ ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) = ( 𝑋 ⊕ ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) )
16	15	adantr	⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ ( Base ‘ 𝑈 ) ) ∧ 𝑄 = ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) → ( 𝑋 ∨ ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) = ( 𝑋 ⊕ ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) )
17		oveq2	⊢ ( 𝑄 = ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) → ( 𝑋 ∨ 𝑄 ) = ( 𝑋 ∨ ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) )
18	17	adantl	⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ ( Base ‘ 𝑈 ) ) ∧ 𝑄 = ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) → ( 𝑋 ∨ 𝑄 ) = ( 𝑋 ∨ ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) )
19		oveq2	⊢ ( 𝑄 = ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) → ( 𝑋 ⊕ 𝑄 ) = ( 𝑋 ⊕ ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) )
20	19	adantl	⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ ( Base ‘ 𝑈 ) ) ∧ 𝑄 = ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) → ( 𝑋 ⊕ 𝑄 ) = ( 𝑋 ⊕ ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) )
21	16 18 20	3eqtr4d	⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ ( Base ‘ 𝑈 ) ) ∧ 𝑄 = ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) → ( 𝑋 ∨ 𝑄 ) = ( 𝑋 ⊕ 𝑄 ) )
22	1 4 7	dvhlmod	⊢ ( 𝜑 → 𝑈 ∈ LMod )
23	10 11 6	islsati	⊢ ( ( 𝑈 ∈ LMod ∧ 𝑄 ∈ 𝐴 ) → ∃ 𝑣 ∈ ( Base ‘ 𝑈 ) 𝑄 = ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) )
24	22 9 23	syl2anc	⊢ ( 𝜑 → ∃ 𝑣 ∈ ( Base ‘ 𝑈 ) 𝑄 = ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) )
25	21 24	r19.29a	⊢ ( 𝜑 → ( 𝑋 ∨ 𝑄 ) = ( 𝑋 ⊕ 𝑄 ) )