Theorem hgmapvvlem2

Description: Lemma for hgmapvv . Eliminate Y (Baer's s). (Contributed by NM, 13-Jun-2015)

	Ref	Expression
Hypotheses	hdmapglem6.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	hdmapglem6.e	$$⊢E=⟨{\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_K},{\mathrm{I}\upharpoonright }_{\mathrm{LTrn}\left(K\right)\left(W\right)}⟩$$
	hdmapglem6.o	$$⊢O=\mathrm{ocH}\left(K\right)\left(W\right)$$
	hdmapglem6.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	hdmapglem6.v	$$⊢V={\mathrm{Base}}_U$$
	hdmapglem6.q	$$⊢\underset{\dot{}}{·}={\cdot }_U$$
	hdmapglem6.r	$$⊢R=\mathrm{Scalar}\left(U\right)$$
	hdmapglem6.b	$$⊢B={\mathrm{Base}}_R$$
	hdmapglem6.t	$$⊢\underset{\dot{}}{\times }={\cdot }_R$$
	hdmapglem6.z	$$⊢\underset{\dot{}}{0}=0_R$$
	hdmapglem6.i	$$⊢\underset{\dot{}}{1}=1_R$$
	hdmapglem6.n	$$⊢N={inv}_r\left(R\right)$$
	hdmapglem6.s	$$⊢S=\mathrm{HDMap}\left(K\right)\left(W\right)$$
	hdmapglem6.g	$$⊢G=\mathrm{HGMap}\left(K\right)\left(W\right)$$
	hdmapglem6.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	hdmapglem6.x	$$⊢\phi \to X\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
	hdmapglem6.c	$$⊢\phi \to C\in O\left(\left\{E\right\}\right)$$
	hdmapglem6.d	$$⊢\phi \to D\in O\left(\left\{E\right\}\right)$$
	hdmapglem6.cd	$$⊢\phi \to S\left(D\right)\left(C\right)=\underset{\dot{}}{1}$$
Assertion	hgmapvvlem2	$$⊢\phi \to G\left(G\left(X\right)\right)=X$$

Proof

Step	Hyp	Ref	Expression
1		hdmapglem6.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		hdmapglem6.e	$$⊢E=⟨{\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_K},{\mathrm{I}\upharpoonright }_{\mathrm{LTrn}\left(K\right)\left(W\right)}⟩$$
3		hdmapglem6.o	$$⊢O=\mathrm{ocH}\left(K\right)\left(W\right)$$
4		hdmapglem6.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
5		hdmapglem6.v	$$⊢V={\mathrm{Base}}_U$$
6		hdmapglem6.q	$$⊢\underset{\dot{}}{·}={\cdot }_U$$
7		hdmapglem6.r	$$⊢R=\mathrm{Scalar}\left(U\right)$$
8		hdmapglem6.b	$$⊢B={\mathrm{Base}}_R$$
9		hdmapglem6.t	$$⊢\underset{\dot{}}{\times }={\cdot }_R$$
10		hdmapglem6.z	$$⊢\underset{\dot{}}{0}=0_R$$
11		hdmapglem6.i	$$⊢\underset{\dot{}}{1}=1_R$$
12		hdmapglem6.n	$$⊢N={inv}_r\left(R\right)$$
13		hdmapglem6.s	$$⊢S=\mathrm{HDMap}\left(K\right)\left(W\right)$$
14		hdmapglem6.g	$$⊢G=\mathrm{HGMap}\left(K\right)\left(W\right)$$
15		hdmapglem6.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
16		hdmapglem6.x	$$⊢\phi \to X\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
17		hdmapglem6.c	$$⊢\phi \to C\in O\left(\left\{E\right\}\right)$$
18		hdmapglem6.d	$$⊢\phi \to D\in O\left(\left\{E\right\}\right)$$
19		hdmapglem6.cd	$$⊢\phi \to S\left(D\right)\left(C\right)=\underset{\dot{}}{1}$$
20	1 4 15	dvhlvec	$$⊢\phi \to U\in \mathrm{LVec}$$
21	7	lvecdrng	$$⊢U\in \mathrm{LVec}\to R\in \mathrm{DivRing}$$
22	20 21	syl	$$⊢\phi \to R\in \mathrm{DivRing}$$
23	16	eldifad	$$⊢\phi \to X\in B$$
24	1 4 7 8 14 15 23	hgmapcl	$$⊢\phi \to G\left(X\right)\in B$$
25		eldifsni	$$⊢X\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\to X\ne \underset{\dot{}}{0}$$
26	16 25	syl	$$⊢\phi \to X\ne \underset{\dot{}}{0}$$
27	1 4 7 8 10 14 15 23	hgmapeq0	$$⊢\phi \to \left(G\left(X\right)=\underset{\dot{}}{0}\leftrightarrow X=\underset{\dot{}}{0}\right)$$
28	27	necon3bid	$$⊢\phi \to \left(G\left(X\right)\ne \underset{\dot{}}{0}\leftrightarrow X\ne \underset{\dot{}}{0}\right)$$
29	26 28	mpbird	$$⊢\phi \to G\left(X\right)\ne \underset{\dot{}}{0}$$
30	8 10 12	drnginvrcl	$$⊢\left(R\in \mathrm{DivRing}\wedge G\left(X\right)\in B\wedge G\left(X\right)\ne \underset{\dot{}}{0}\right)\to N\left(G\left(X\right)\right)\in B$$
31	22 24 29 30	syl3anc	$$⊢\phi \to N\left(G\left(X\right)\right)\in B$$
32	8 10 12	drnginvrn0	$$⊢\left(R\in \mathrm{DivRing}\wedge G\left(X\right)\in B\wedge G\left(X\right)\ne \underset{\dot{}}{0}\right)\to N\left(G\left(X\right)\right)\ne \underset{\dot{}}{0}$$
33	22 24 29 32	syl3anc	$$⊢\phi \to N\left(G\left(X\right)\right)\ne \underset{\dot{}}{0}$$
34		eldifsn	$$⊢N\left(G\left(X\right)\right)\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\leftrightarrow \left(N\left(G\left(X\right)\right)\in B\wedge N\left(G\left(X\right)\right)\ne \underset{\dot{}}{0}\right)$$
35	31 33 34	sylanbrc	$$⊢\phi \to N\left(G\left(X\right)\right)\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
36	8 10 9 11 12	drnginvrl	$$⊢\left(R\in \mathrm{DivRing}\wedge G\left(X\right)\in B\wedge G\left(X\right)\ne \underset{\dot{}}{0}\right)\to N\left(G\left(X\right)\right)\underset{\dot{}}{\times }G\left(X\right)=\underset{\dot{}}{1}$$
37	22 24 29 36	syl3anc	$$⊢\phi \to N\left(G\left(X\right)\right)\underset{\dot{}}{\times }G\left(X\right)=\underset{\dot{}}{1}$$
38	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 35 37	hgmapvvlem1	$$⊢\phi \to G\left(G\left(X\right)\right)=X$$