mapdpglem21

	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\})$
	mapdpglem4.q	$⊢ Q = 0_{U}$
	mapdpglem.ne	$⊢ φ \to N (\{X\}) \neq N (\{Y\})$
	mapdpglem4.jt	$⊢ φ \to M (N (\{X \underset{˙}{-} Y\})) = J (\{t\})$
	mapdpglem4.z	$⊢ \underset{˙}{0} = 0_{A}$
	mapdpglem4.g4	$⊢ φ \to g \in B$
	mapdpglem4.z4	$⊢ φ \to z \in M (N (\{Y\}))$
	mapdpglem4.t4	$⊢ φ \to t = (g \underset{˙}{\cdot} G) R z$
	mapdpglem4.xn	$⊢ φ \to X \neq Q$
	mapdpglem12.yn	$⊢ φ \to Y \neq Q$
	mapdpglem17.ep	$⊢ E = {inv}_{r} (A) (g) \underset{˙}{\cdot} z$
Assertion	mapdpglem21	$⊢ φ \to {inv}_{r} (A) (g) \underset{˙}{\cdot} t = G R E$

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		mapdpglem4.q	$⊢ Q = 0_{U}$
22		mapdpglem.ne	$⊢ φ \to N (\{X\}) \neq N (\{Y\})$
23		mapdpglem4.jt	$⊢ φ \to M (N (\{X \underset{˙}{-} Y\})) = J (\{t\})$
24		mapdpglem4.z	$⊢ \underset{˙}{0} = 0_{A}$
25		mapdpglem4.g4	$⊢ φ \to g \in B$
26		mapdpglem4.z4	$⊢ φ \to z \in M (N (\{Y\}))$
27		mapdpglem4.t4	$⊢ φ \to t = (g \underset{˙}{\cdot} G) R z$
28		mapdpglem4.xn	$⊢ φ \to X \neq Q$
29		mapdpglem12.yn	$⊢ φ \to Y \neq Q$
30		mapdpglem17.ep	$⊢ E = {inv}_{r} (A) (g) \underset{˙}{\cdot} z$
31	27	oveq2d	$⊢ φ \to {inv}_{r} (A) (g) \underset{˙}{\cdot} t = {inv}_{r} (A) (g) \underset{˙}{\cdot} ((g \underset{˙}{\cdot} G) R z)$
32		eqid	$⊢ Scalar (C) = Scalar (C)$
33		eqid	$⊢ {Base}_{Scalar (C)} = {Base}_{Scalar (C)}$
34	1 7 8	lcdlmod	$⊢ φ \to C \in LMod$
35	1 3 8	dvhlvec	$⊢ φ \to U \in LVec$
36	15	lvecdrng	$⊢ U \in LVec \to A \in DivRing$
37	35 36	syl	$⊢ φ \to A \in DivRing$
38	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28	mapdpglem11	$⊢ φ \to g \neq \underset{˙}{0}$
39		eqid	$⊢ {inv}_{r} (A) = {inv}_{r} (A)$
40	16 24 39	drnginvrcl	$⊢ (A \in DivRing \land g \in B \land g \neq \underset{˙}{0}) \to {inv}_{r} (A) (g) \in B$
41	37 25 38 40	syl3anc	$⊢ φ \to {inv}_{r} (A) (g) \in B$
42	1 3 15 16 7 32 33 8	lcdsbase	$⊢ φ \to {Base}_{Scalar (C)} = B$
43	41 42	eleqtrrd	$⊢ φ \to {inv}_{r} (A) (g) \in {Base}_{Scalar (C)}$
44	1 3 15 16 7 13 17 8 25 19	lcdvscl	$⊢ φ \to g \underset{˙}{\cdot} G \in F$
45		eqid	$⊢ LSubSp (U) = LSubSp (U)$
46		eqid	$⊢ LSubSp (C) = LSubSp (C)$
47	1 3 8	dvhlmod	$⊢ φ \to U \in LMod$
48	4 45 6	lspsncl	$⊢ (U \in LMod \land Y \in V) \to N (\{Y\}) \in LSubSp (U)$
49	47 10 48	syl2anc	$⊢ φ \to N (\{Y\}) \in LSubSp (U)$
50	1 2 3 45 7 46 8 49	mapdcl2	$⊢ φ \to M (N (\{Y\})) \in LSubSp (C)$
51	13 46	lssss	$⊢ M (N (\{Y\})) \in LSubSp (C) \to M (N (\{Y\})) \subseteq F$
52	50 51	syl	$⊢ φ \to M (N (\{Y\})) \subseteq F$
53	52 26	sseldd	$⊢ φ \to z \in F$
54	13 17 32 33 18 34 43 44 53	lmodsubdi	$⊢ φ \to {inv}_{r} (A) (g) \underset{˙}{\cdot} ((g \underset{˙}{\cdot} G) R z) = ({inv}_{r} (A) (g) \underset{˙}{\cdot} (g \underset{˙}{\cdot} G)) R ({inv}_{r} (A) (g) \underset{˙}{\cdot} z)$
55		eqid	$⊢ \cdot_{A} = \cdot_{A}$
56		eqid	$⊢ 1_{A} = 1_{A}$
57	16 24 55 56 39	drnginvrr	$⊢ (A \in DivRing \land g \in B \land g \neq \underset{˙}{0}) \to g \cdot_{A} {inv}_{r} (A) (g) = 1_{A}$
58	37 25 38 57	syl3anc	$⊢ φ \to g \cdot_{A} {inv}_{r} (A) (g) = 1_{A}$
59		eqid	$⊢ 1_{Scalar (C)} = 1_{Scalar (C)}$
60	1 3 15 56 7 32 59 8	lcd1	$⊢ φ \to 1_{Scalar (C)} = 1_{A}$
61	58 60	eqtr4d	$⊢ φ \to g \cdot_{A} {inv}_{r} (A) (g) = 1_{Scalar (C)}$
62	61	oveq1d	$⊢ φ \to (g \cdot_{A} {inv}_{r} (A) (g)) \underset{˙}{\cdot} G = 1_{Scalar (C)} \underset{˙}{\cdot} G$
63	1 3 15 16 55 7 13 17 8 41 25 19	lcdvsass	$⊢ φ \to (g \cdot_{A} {inv}_{r} (A) (g)) \underset{˙}{\cdot} G = {inv}_{r} (A) (g) \underset{˙}{\cdot} (g \underset{˙}{\cdot} G)$
64	13 32 17 59	lmodvs1	$⊢ (C \in LMod \land G \in F) \to 1_{Scalar (C)} \underset{˙}{\cdot} G = G$
65	34 19 64	syl2anc	$⊢ φ \to 1_{Scalar (C)} \underset{˙}{\cdot} G = G$
66	62 63 65	3eqtr3d	$⊢ φ \to {inv}_{r} (A) (g) \underset{˙}{\cdot} (g \underset{˙}{\cdot} G) = G$
67	66	oveq1d	$⊢ φ \to ({inv}_{r} (A) (g) \underset{˙}{\cdot} (g \underset{˙}{\cdot} G)) R ({inv}_{r} (A) (g) \underset{˙}{\cdot} z) = G R ({inv}_{r} (A) (g) \underset{˙}{\cdot} z)$
68	30	oveq2i	$⊢ G R E = G R ({inv}_{r} (A) (g) \underset{˙}{\cdot} z)$
69	67 68	eqtr4di	$⊢ φ \to ({inv}_{r} (A) (g) \underset{˙}{\cdot} (g \underset{˙}{\cdot} G)) R ({inv}_{r} (A) (g) \underset{˙}{\cdot} z) = G R E$
70	31 54 69	3eqtrd	$⊢ φ \to {inv}_{r} (A) (g) \underset{˙}{\cdot} t = G R E$

Metamath Proof Explorer

Theorem mapdpglem21

Proof