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	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	hdmapip0com.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	hdmapip0com.v	$$⊢V={\mathrm{Base}}_U$$
	hdmapip0com.r	$$⊢R=\mathrm{Scalar}\left(U\right)$$
	hdmapip0com.z	$$⊢\underset{\dot{}}{0}=0_R$$
	hdmapip0com.s	$$⊢S=\mathrm{HDMap}\left(K\right)\left(W\right)$$
	hdmapip0com.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	hdmapip0com.x	$$⊢\phi \to X\in V$$
	hdmapip0com.y	$$⊢\phi \to Y\in V$$
Assertion	hdmapip0com	$$⊢\phi \to \left(S\left(X\right)\left(Y\right)=\underset{\dot{}}{0}\leftrightarrow S\left(Y\right)\left(X\right)=\underset{\dot{}}{0}\right)$$

Proof

Step	Hyp	Ref	Expression
1		hdmapip0com.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		hdmapip0com.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
3		hdmapip0com.v	$$⊢V={\mathrm{Base}}_U$$
4		hdmapip0com.r	$$⊢R=\mathrm{Scalar}\left(U\right)$$
5		hdmapip0com.z	$$⊢\underset{\dot{}}{0}=0_R$$
6		hdmapip0com.s	$$⊢S=\mathrm{HDMap}\left(K\right)\left(W\right)$$
7		hdmapip0com.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
8		hdmapip0com.x	$$⊢\phi \to X\in V$$
9		hdmapip0com.y	$$⊢\phi \to Y\in V$$
10		eqid	$$⊢\mathrm{ocH}\left(K\right)\left(W\right)=\mathrm{ocH}\left(K\right)\left(W\right)$$
11	1 10 2 3 7 9 8	dochsncom	$$⊢\phi \to \left(Y\in \mathrm{ocH}\left(K\right)\left(W\right)\left(\left\{X\right\}\right)\leftrightarrow X\in \mathrm{ocH}\left(K\right)\left(W\right)\left(\left\{Y\right\}\right)\right)$$
12	1 10 2 3 4 5 6 7 8 9	hdmapellkr	$$⊢\phi \to \left(S\left(X\right)\left(Y\right)=\underset{\dot{}}{0}\leftrightarrow Y\in \mathrm{ocH}\left(K\right)\left(W\right)\left(\left\{X\right\}\right)\right)$$
13	1 10 2 3 4 5 6 7 9 8	hdmapellkr	$$⊢\phi \to \left(S\left(Y\right)\left(X\right)=\underset{\dot{}}{0}\leftrightarrow X\in \mathrm{ocH}\left(K\right)\left(W\right)\left(\left\{Y\right\}\right)\right)$$
14	11 12 13	3bitr4d	$$⊢\phi \to \left(S\left(X\right)\left(Y\right)=\underset{\dot{}}{0}\leftrightarrow S\left(Y\right)\left(X\right)=\underset{\dot{}}{0}\right)$$