mapdpglem3

Description: Lemma for mapdpg . Baer p. 45, line 3: "infer ... the existence of a number g in G and of an element z in (Fy)* such that t = gx'-z." (We scope $d g w z ph locally to avoid clashes with later substitutions into ph .) (Contributed by NM, 18-Mar-2015)

	Ref	Expression
Hypotheses	mapdpglem.h	$⊢ H = LHyp (K)$
	mapdpglem.m	$⊢ M = mapd (K) (W)$
	mapdpglem.u	$⊢ U = DVecH (K) (W)$
	mapdpglem.v	$⊢ V = {Base}_{U}$
	mapdpglem.s	$⊢ \underset{˙}{-} = -_{U}$
	mapdpglem.n	$⊢ N = LSpan (U)$
	mapdpglem.c	$⊢ C = LCDual (K) (W)$
	mapdpglem.k	$⊢ φ \to (K \in HL \land W \in H)$
	mapdpglem.x	$⊢ φ \to X \in V$
	mapdpglem.y	$⊢ φ \to Y \in V$
	mapdpglem1.p	$⊢ \underset{˙}{\oplus} = LSSum (C)$
	mapdpglem2.j	$⊢ J = LSpan (C)$
	mapdpglem3.f	$⊢ F = {Base}_{C}$
	mapdpglem3.te	$⊢ φ \to t \in (M (N (\{X\})) \underset{˙}{\oplus} M (N (\{Y\})))$
	mapdpglem3.a	$⊢ A = Scalar (U)$
	mapdpglem3.b	$⊢ B = {Base}_{A}$
	mapdpglem3.t	$⊢ \underset{˙}{\cdot} = \cdot_{C}$
	mapdpglem3.r	$⊢ R = -_{C}$
	mapdpglem3.g	$⊢ φ \to G \in F$
	mapdpglem3.e	$⊢ φ \to M (N (\{X\})) = J (\{G\})$
Assertion	mapdpglem3	$⊢ φ \to \exists g \in B \exists z \in M (N (\{Y\})) t = (g \underset{˙}{\cdot} G) R z$

Proof

Step	Hyp	Ref	Expression
1		mapdpglem.h	$⊢ H = LHyp (K)$
2		mapdpglem.m	$⊢ M = mapd (K) (W)$
3		mapdpglem.u	$⊢ U = DVecH (K) (W)$
4		mapdpglem.v	$⊢ V = {Base}_{U}$
5		mapdpglem.s	$⊢ \underset{˙}{-} = -_{U}$
6		mapdpglem.n	$⊢ N = LSpan (U)$
7		mapdpglem.c	$⊢ C = LCDual (K) (W)$
8		mapdpglem.k	$⊢ φ \to (K \in HL \land W \in H)$
9		mapdpglem.x	$⊢ φ \to X \in V$
10		mapdpglem.y	$⊢ φ \to Y \in V$
11		mapdpglem1.p	$⊢ \underset{˙}{\oplus} = LSSum (C)$
12		mapdpglem2.j	$⊢ J = LSpan (C)$
13		mapdpglem3.f	$⊢ F = {Base}_{C}$
14		mapdpglem3.te	$⊢ φ \to t \in (M (N (\{X\})) \underset{˙}{\oplus} M (N (\{Y\})))$
15		mapdpglem3.a	$⊢ A = Scalar (U)$
16		mapdpglem3.b	$⊢ B = {Base}_{A}$
17		mapdpglem3.t	$⊢ \underset{˙}{\cdot} = \cdot_{C}$
18		mapdpglem3.r	$⊢ R = -_{C}$
19		mapdpglem3.g	$⊢ φ \to G \in F$
20		mapdpglem3.e	$⊢ φ \to M (N (\{X\})) = J (\{G\})$
21	20	oveq1d	$⊢ φ \to M (N (\{X\})) \underset{˙}{\oplus} M (N (\{Y\})) = J (\{G\}) \underset{˙}{\oplus} M (N (\{Y\}))$
22	14 21	eleqtrd	$⊢ φ \to t \in (J (\{G\}) \underset{˙}{\oplus} M (N (\{Y\})))$
23		r19.41v	$⊢ \exists g \in B (w = g \underset{˙}{\cdot} G \land \exists z \in M (N (\{Y\})) t = w R z) \leftrightarrow (\exists g \in B w = g \underset{˙}{\cdot} G \land \exists z \in M (N (\{Y\})) t = w R z)$
24	1 7 8	lcdlmod	$⊢ φ \to C \in LMod$
25		eqid	$⊢ Scalar (C) = Scalar (C)$
26		eqid	$⊢ {Base}_{Scalar (C)} = {Base}_{Scalar (C)}$
27	25 26 13 17 12	ellspsn	$⊢ (C \in LMod \land G \in F) \to (w \in J (\{G\}) \leftrightarrow \exists g \in {Base}_{Scalar (C)} w = g \underset{˙}{\cdot} G)$
28	24 19 27	syl2anc	$⊢ φ \to (w \in J (\{G\}) \leftrightarrow \exists g \in {Base}_{Scalar (C)} w = g \underset{˙}{\cdot} G)$
29	1 3 15 16 7 25 26 8	lcdsbase	$⊢ φ \to {Base}_{Scalar (C)} = B$
30	29	rexeqdv	$⊢ φ \to (\exists g \in {Base}_{Scalar (C)} w = g \underset{˙}{\cdot} G \leftrightarrow \exists g \in B w = g \underset{˙}{\cdot} G)$
31	28 30	bitrd	$⊢ φ \to (w \in J (\{G\}) \leftrightarrow \exists g \in B w = g \underset{˙}{\cdot} G)$
32	31	anbi1d	$⊢ φ \to ((w \in J (\{G\}) \land \exists z \in M (N (\{Y\})) t = w R z) \leftrightarrow (\exists g \in B w = g \underset{˙}{\cdot} G \land \exists z \in M (N (\{Y\})) t = w R z))$
33	23 32	bitr4id	$⊢ φ \to (\exists g \in B (w = g \underset{˙}{\cdot} G \land \exists z \in M (N (\{Y\})) t = w R z) \leftrightarrow (w \in J (\{G\}) \land \exists z \in M (N (\{Y\})) t = w R z))$
34	33	exbidv	$⊢ φ \to (\exists w \exists g \in B (w = g \underset{˙}{\cdot} G \land \exists z \in M (N (\{Y\})) t = w R z) \leftrightarrow \exists w (w \in J (\{G\}) \land \exists z \in M (N (\{Y\})) t = w R z))$
35		df-rex	$⊢ \exists w \in J (\{G\}) \exists z \in M (N (\{Y\})) t = w R z \leftrightarrow \exists w (w \in J (\{G\}) \land \exists z \in M (N (\{Y\})) t = w R z)$
36	34 35	bitr4di	$⊢ φ \to (\exists w \exists g \in B (w = g \underset{˙}{\cdot} G \land \exists z \in M (N (\{Y\})) t = w R z) \leftrightarrow \exists w \in J (\{G\}) \exists z \in M (N (\{Y\})) t = w R z)$
37		eqid	$⊢ LSubSp (C) = LSubSp (C)$
38	37	lsssssubg	$⊢ C \in LMod \to LSubSp (C) \subseteq SubGrp (C)$
39	24 38	syl	$⊢ φ \to LSubSp (C) \subseteq SubGrp (C)$
40	13 37 12	lspsncl	$⊢ (C \in LMod \land G \in F) \to J (\{G\}) \in LSubSp (C)$
41	24 19 40	syl2anc	$⊢ φ \to J (\{G\}) \in LSubSp (C)$
42	39 41	sseldd	$⊢ φ \to J (\{G\}) \in SubGrp (C)$
43		eqid	$⊢ LSubSp (U) = LSubSp (U)$
44	1 3 8	dvhlmod	$⊢ φ \to U \in LMod$
45	4 43 6	lspsncl	$⊢ (U \in LMod \land Y \in V) \to N (\{Y\}) \in LSubSp (U)$
46	44 10 45	syl2anc	$⊢ φ \to N (\{Y\}) \in LSubSp (U)$
47	1 2 3 43 7 37 8 46	mapdcl2	$⊢ φ \to M (N (\{Y\})) \in LSubSp (C)$
48	39 47	sseldd	$⊢ φ \to M (N (\{Y\})) \in SubGrp (C)$
49	18 11 42 48	lsmelvalm	$⊢ φ \to (t \in (J (\{G\}) \underset{˙}{\oplus} M (N (\{Y\}))) \leftrightarrow \exists w \in J (\{G\}) \exists z \in M (N (\{Y\})) t = w R z)$
50	36 49	bitr4d	$⊢ φ \to (\exists w \exists g \in B (w = g \underset{˙}{\cdot} G \land \exists z \in M (N (\{Y\})) t = w R z) \leftrightarrow t \in (J (\{G\}) \underset{˙}{\oplus} M (N (\{Y\}))))$
51	22 50	mpbird	$⊢ φ \to \exists w \exists g \in B (w = g \underset{˙}{\cdot} G \land \exists z \in M (N (\{Y\})) t = w R z)$
52		ovex	$⊢ g \underset{˙}{\cdot} G \in V$
53		oveq1	$⊢ w = g \underset{˙}{\cdot} G \to w R z = (g \underset{˙}{\cdot} G) R z$
54	53	eqeq2d	$⊢ w = g \underset{˙}{\cdot} G \to (t = w R z \leftrightarrow t = (g \underset{˙}{\cdot} G) R z)$
55	54	rexbidv	$⊢ w = g \underset{˙}{\cdot} G \to (\exists z \in M (N (\{Y\})) t = w R z \leftrightarrow \exists z \in M (N (\{Y\})) t = (g \underset{˙}{\cdot} G) R z)$
56	52 55	ceqsexv	$⊢ \exists w (w = g \underset{˙}{\cdot} G \land \exists z \in M (N (\{Y\})) t = w R z) \leftrightarrow \exists z \in M (N (\{Y\})) t = (g \underset{˙}{\cdot} G) R z$
57	56	rexbii	$⊢ \exists g \in B \exists w (w = g \underset{˙}{\cdot} G \land \exists z \in M (N (\{Y\})) t = w R z) \leftrightarrow \exists g \in B \exists z \in M (N (\{Y\})) t = (g \underset{˙}{\cdot} G) R z$
58		rexcom4	$⊢ \exists g \in B \exists w (w = g \underset{˙}{\cdot} G \land \exists z \in M (N (\{Y\})) t = w R z) \leftrightarrow \exists w \exists g \in B (w = g \underset{˙}{\cdot} G \land \exists z \in M (N (\{Y\})) t = w R z)$
59	57 58	bitr3i	$⊢ \exists g \in B \exists z \in M (N (\{Y\})) t = (g \underset{˙}{\cdot} G) R z \leftrightarrow \exists w \exists g \in B (w = g \underset{˙}{\cdot} G \land \exists z \in M (N (\{Y\})) t = w R z)$
60	51 59	sylibr	$⊢ φ \to \exists g \in B \exists z \in M (N (\{Y\})) t = (g \underset{˙}{\cdot} G) R z$

Metamath Proof Explorer

Theorem mapdpglem3

Proof