Theorem mapdpglem27

Description: Lemma for mapdpg . Baer p. 45 line 16: "v(x'-y'') = x'-y'" (with equality swapped). (Contributed by NM, 22-Mar-2015)

	Ref	Expression
Hypotheses	mapdpg.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	mapdpg.m	$$⊢M=\mathrm{mapd}\left(K\right)\left(W\right)$$
	mapdpg.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	mapdpg.v	$$⊢V={\mathrm{Base}}_U$$
	mapdpg.s	$$⊢\underset{\dot{}}{-}={-}_U$$
	mapdpg.z	$$⊢\underset{\dot{}}{0}=0_U$$
	mapdpg.n	$$⊢N=\mathrm{LSpan}\left(U\right)$$
	mapdpg.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
	mapdpg.f	$$⊢F={\mathrm{Base}}_C$$
	mapdpg.r	$$⊢R={-}_C$$
	mapdpg.j	$$⊢J=\mathrm{LSpan}\left(C\right)$$
	mapdpg.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	mapdpg.x	$$⊢\phi \to X\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
	mapdpg.y	$$⊢\phi \to Y\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
	mapdpg.g	$$⊢\phi \to G\in F$$
	mapdpg.ne	$$⊢\phi \to N\left(\left\{X\right\}\right)\ne N\left(\left\{Y\right\}\right)$$
	mapdpg.e	$$⊢\phi \to M\left(N\left(\left\{X\right\}\right)\right)=J\left(\left\{G\right\}\right)$$
	mapdpgem25.h1	$$⊢\phi \to \left(h\in F\wedge \left(M\left(N\left(\left\{Y\right\}\right)\right)=J\left(\left\{h\right\}\right)\wedge M\left(N\left(\left\{X\underset{\dot{}}{-}Y\right\}\right)\right)=J\left(\left\{GRh\right\}\right)\right)\right)$$
	mapdpgem25.i1	$$⊢\phi \to \left(i\in F\wedge \left(M\left(N\left(\left\{Y\right\}\right)\right)=J\left(\left\{i\right\}\right)\wedge M\left(N\left(\left\{X\underset{\dot{}}{-}Y\right\}\right)\right)=J\left(\left\{GRi\right\}\right)\right)\right)$$
	mapdpglem26.a	$$⊢A=\mathrm{Scalar}\left(U\right)$$
	mapdpglem26.b	$$⊢B={\mathrm{Base}}_A$$
	mapdpglem26.t	$$⊢\underset{\dot{}}{·}={\cdot }_C$$
	mapdpglem26.o	$$⊢O=0_A$$
Assertion	mapdpglem27	$$⊢\phi \to \exists v\in \left(B\setminus \left\{O\right\}\right)GRh=v\underset{\dot{}}{·}\left(GRi\right)$$

Proof

Step	Hyp	Ref	Expression
1		mapdpg.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		mapdpg.m	$$⊢M=\mathrm{mapd}\left(K\right)\left(W\right)$$
3		mapdpg.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
4		mapdpg.v	$$⊢V={\mathrm{Base}}_U$$
5		mapdpg.s	$$⊢\underset{\dot{}}{-}={-}_U$$
6		mapdpg.z	$$⊢\underset{\dot{}}{0}=0_U$$
7		mapdpg.n	$$⊢N=\mathrm{LSpan}\left(U\right)$$
8		mapdpg.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
9		mapdpg.f	$$⊢F={\mathrm{Base}}_C$$
10		mapdpg.r	$$⊢R={-}_C$$
11		mapdpg.j	$$⊢J=\mathrm{LSpan}\left(C\right)$$
12		mapdpg.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
13		mapdpg.x	$$⊢\phi \to X\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
14		mapdpg.y	$$⊢\phi \to Y\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
15		mapdpg.g	$$⊢\phi \to G\in F$$
16		mapdpg.ne	$$⊢\phi \to N\left(\left\{X\right\}\right)\ne N\left(\left\{Y\right\}\right)$$
17		mapdpg.e	$$⊢\phi \to M\left(N\left(\left\{X\right\}\right)\right)=J\left(\left\{G\right\}\right)$$
18		mapdpgem25.h1	$$⊢\phi \to \left(h\in F\wedge \left(M\left(N\left(\left\{Y\right\}\right)\right)=J\left(\left\{h\right\}\right)\wedge M\left(N\left(\left\{X\underset{\dot{}}{-}Y\right\}\right)\right)=J\left(\left\{GRh\right\}\right)\right)\right)$$
19		mapdpgem25.i1	$$⊢\phi \to \left(i\in F\wedge \left(M\left(N\left(\left\{Y\right\}\right)\right)=J\left(\left\{i\right\}\right)\wedge M\left(N\left(\left\{X\underset{\dot{}}{-}Y\right\}\right)\right)=J\left(\left\{GRi\right\}\right)\right)\right)$$
20		mapdpglem26.a	$$⊢A=\mathrm{Scalar}\left(U\right)$$
21		mapdpglem26.b	$$⊢B={\mathrm{Base}}_A$$
22		mapdpglem26.t	$$⊢\underset{\dot{}}{·}={\cdot }_C$$
23		mapdpglem26.o	$$⊢O=0_A$$
24	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19	mapdpglem25	$$⊢\phi \to \left(J\left(\left\{h\right\}\right)=J\left(\left\{i\right\}\right)\wedge J\left(\left\{GRh\right\}\right)=J\left(\left\{GRi\right\}\right)\right)$$
25	24	simprd	$$⊢\phi \to J\left(\left\{GRh\right\}\right)=J\left(\left\{GRi\right\}\right)$$
26		eqid	$$⊢\mathrm{Scalar}\left(C\right)=\mathrm{Scalar}\left(C\right)$$
27		eqid	$$⊢{\mathrm{Base}}_{\mathrm{Scalar}\left(C\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(C\right)}$$
28		eqid	$$⊢0_{\mathrm{Scalar}\left(C\right)}=0_{\mathrm{Scalar}\left(C\right)}$$
29	1 8 12	lcdlvec	$$⊢\phi \to C\in \mathrm{LVec}$$
30	1 8 12	lcdlmod	$$⊢\phi \to C\in \mathrm{LMod}$$
31	18	simpld	$$⊢\phi \to h\in F$$
32	9 10	lmodvsubcl	$$⊢\left(C\in \mathrm{LMod}\wedge G\in F\wedge h\in F\right)\to GRh\in F$$
33	30 15 31 32	syl3anc	$$⊢\phi \to GRh\in F$$
34	19	simpld	$$⊢\phi \to i\in F$$
35	9 10	lmodvsubcl	$$⊢\left(C\in \mathrm{LMod}\wedge G\in F\wedge i\in F\right)\to GRi\in F$$
36	30 15 34 35	syl3anc	$$⊢\phi \to GRi\in F$$
37	9 26 27 28 22 11 29 33 36	lspsneq	$$⊢\phi \to \left(J\left(\left\{GRh\right\}\right)=J\left(\left\{GRi\right\}\right)\leftrightarrow \exists v\in \left({\mathrm{Base}}_{\mathrm{Scalar}\left(C\right)}\setminus \left\{0_{\mathrm{Scalar}\left(C\right)}\right\}\right)GRh=v\underset{\dot{}}{·}\left(GRi\right)\right)$$
38	1 3 20 21 8 26 27 12	lcdsbase	$$⊢\phi \to {\mathrm{Base}}_{\mathrm{Scalar}\left(C\right)}=B$$
39	1 3 20 23 8 26 28 12	lcd0	$$⊢\phi \to 0_{\mathrm{Scalar}\left(C\right)}=O$$
40	39	sneqd	$$⊢\phi \to \left\{0_{\mathrm{Scalar}\left(C\right)}\right\}=\left\{O\right\}$$
41	38 40	difeq12d	$$⊢\phi \to {\mathrm{Base}}_{\mathrm{Scalar}\left(C\right)}\setminus \left\{0_{\mathrm{Scalar}\left(C\right)}\right\}=B\setminus \left\{O\right\}$$
42	41	rexeqdv	$$⊢\phi \to \left(\exists v\in \left({\mathrm{Base}}_{\mathrm{Scalar}\left(C\right)}\setminus \left\{0_{\mathrm{Scalar}\left(C\right)}\right\}\right)GRh=v\underset{\dot{}}{·}\left(GRi\right)\leftrightarrow \exists v\in \left(B\setminus \left\{O\right\}\right)GRh=v\underset{\dot{}}{·}\left(GRi\right)\right)$$
43	37 42	bitrd	$$⊢\phi \to \left(J\left(\left\{GRh\right\}\right)=J\left(\left\{GRi\right\}\right)\leftrightarrow \exists v\in \left(B\setminus \left\{O\right\}\right)GRh=v\underset{\dot{}}{·}\left(GRi\right)\right)$$
44	25 43	mpbid	$$⊢\phi \to \exists v\in \left(B\setminus \left\{O\right\}\right)GRh=v\underset{\dot{}}{·}\left(GRi\right)$$