Theorem hdmapip0com

Description: Commutation property of Baer's sigma map (Holland's A map). Line 20 of Holland95 p. 14. Also part of Lemma 1 of Baer p. 110 line 7. (Contributed by NM, 9-Jun-2015)

	Ref	Expression
Hypotheses	hdmapip0com.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	hdmapip0com.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	hdmapip0com.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
	hdmapip0com.r	⊢ 𝑅 = ( Scalar ‘ 𝑈 )
	hdmapip0com.z	⊢ 0 = ( 0g ‘ 𝑅 )
	hdmapip0com.s	⊢ 𝑆 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
	hdmapip0com.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
	hdmapip0com.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
	hdmapip0com.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
Assertion	hdmapip0com	⊢ ( 𝜑 → ( ( ( 𝑆 ‘ 𝑋 ) ‘ 𝑌 ) = 0 ↔ ( ( 𝑆 ‘ 𝑌 ) ‘ 𝑋 ) = 0 ) )

Proof

Step	Hyp	Ref	Expression
1		hdmapip0com.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		hdmapip0com.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3		hdmapip0com.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
4		hdmapip0com.r	⊢ 𝑅 = ( Scalar ‘ 𝑈 )
5		hdmapip0com.z	⊢ 0 = ( 0g ‘ 𝑅 )
6		hdmapip0com.s	⊢ 𝑆 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
7		hdmapip0com.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
8		hdmapip0com.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
9		hdmapip0com.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
10		eqid	⊢ ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
11	1 10 2 3 7 9 8	dochsncom	⊢ ( 𝜑 → ( 𝑌 ∈ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ { 𝑋 } ) ↔ 𝑋 ∈ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ { 𝑌 } ) ) )
12	1 10 2 3 4 5 6 7 8 9	hdmapellkr	⊢ ( 𝜑 → ( ( ( 𝑆 ‘ 𝑋 ) ‘ 𝑌 ) = 0 ↔ 𝑌 ∈ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ { 𝑋 } ) ) )
13	1 10 2 3 4 5 6 7 9 8	hdmapellkr	⊢ ( 𝜑 → ( ( ( 𝑆 ‘ 𝑌 ) ‘ 𝑋 ) = 0 ↔ 𝑋 ∈ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ { 𝑌 } ) ) )
14	11 12 13	3bitr4d	⊢ ( 𝜑 → ( ( ( 𝑆 ‘ 𝑋 ) ‘ 𝑌 ) = 0 ↔ ( ( 𝑆 ‘ 𝑌 ) ‘ 𝑋 ) = 0 ) )