mapdpglem30

Description: Lemma for mapdpg . Baer p. 45 line 18: "Hence we deduce (from mapdpglem28 , using lvecindp2 ) that v = 1 and v = u...". TODO: would it be shorter to have only the v = ( 1rA ) part and use mapdpglem28.u2 in mapdpglem31 ? (Contributed by NM, 22-Mar-2015)

	Ref	Expression
Hypotheses	mapdpg.h	$⊢ H = LHyp (K)$
	mapdpg.m	$⊢ M = mapd (K) (W)$
	mapdpg.u	$⊢ U = DVecH (K) (W)$
	mapdpg.v	$⊢ V = {Base}_{U}$
	mapdpg.s	$⊢ \underset{˙}{-} = -_{U}$
	mapdpg.z	$⊢ \underset{˙}{0} = 0_{U}$
	mapdpg.n	$⊢ N = LSpan (U)$
	mapdpg.c	$⊢ C = LCDual (K) (W)$
	mapdpg.f	$⊢ F = {Base}_{C}$
	mapdpg.r	$⊢ R = -_{C}$
	mapdpg.j	$⊢ J = LSpan (C)$
	mapdpg.k	$⊢ φ \to (K \in HL \land W \in H)$
	mapdpg.x	$⊢ φ \to X \in (V ∖ \{\underset{˙}{0}\})$
	mapdpg.y	$⊢ φ \to Y \in (V ∖ \{\underset{˙}{0}\})$
	mapdpg.g	$⊢ φ \to G \in F$
	mapdpg.ne	$⊢ φ \to N (\{X\}) \neq N (\{Y\})$
	mapdpg.e	$⊢ φ \to M (N (\{X\})) = J (\{G\})$
	mapdpgem25.h1	$⊢ φ \to (h \in F \land (M (N (\{Y\})) = J (\{h\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{G R h\})))$
	mapdpgem25.i1	$⊢ φ \to (i \in F \land (M (N (\{Y\})) = J (\{i\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{G R i\})))$
	mapdpglem26.a	$⊢ A = Scalar (U)$
	mapdpglem26.b	$⊢ B = {Base}_{A}$
	mapdpglem26.t	$⊢ \underset{˙}{\cdot} = \cdot_{C}$
	mapdpglem26.o	$⊢ O = 0_{A}$
	mapdpglem28.ve	$⊢ φ \to v \in B$
	mapdpglem28.u1	$⊢ φ \to h = u \underset{˙}{\cdot} i$
	mapdpglem28.u2	$⊢ φ \to G R h = v \underset{˙}{\cdot} (G R i)$
	mapdpglem28.ue	$⊢ φ \to u \in B$
Assertion	mapdpglem30	$⊢ φ \to (v = 1_{A} \land v = u)$

Proof

Step	Hyp	Ref	Expression
1		mapdpg.h	$⊢ H = LHyp (K)$
2		mapdpg.m	$⊢ M = mapd (K) (W)$
3		mapdpg.u	$⊢ U = DVecH (K) (W)$
4		mapdpg.v	$⊢ V = {Base}_{U}$
5		mapdpg.s	$⊢ \underset{˙}{-} = -_{U}$
6		mapdpg.z	$⊢ \underset{˙}{0} = 0_{U}$
7		mapdpg.n	$⊢ N = LSpan (U)$
8		mapdpg.c	$⊢ C = LCDual (K) (W)$
9		mapdpg.f	$⊢ F = {Base}_{C}$
10		mapdpg.r	$⊢ R = -_{C}$
11		mapdpg.j	$⊢ J = LSpan (C)$
12		mapdpg.k	$⊢ φ \to (K \in HL \land W \in H)$
13		mapdpg.x	$⊢ φ \to X \in (V ∖ \{\underset{˙}{0}\})$
14		mapdpg.y	$⊢ φ \to Y \in (V ∖ \{\underset{˙}{0}\})$
15		mapdpg.g	$⊢ φ \to G \in F$
16		mapdpg.ne	$⊢ φ \to N (\{X\}) \neq N (\{Y\})$
17		mapdpg.e	$⊢ φ \to M (N (\{X\})) = J (\{G\})$
18		mapdpgem25.h1	$⊢ φ \to (h \in F \land (M (N (\{Y\})) = J (\{h\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{G R h\})))$
19		mapdpgem25.i1	$⊢ φ \to (i \in F \land (M (N (\{Y\})) = J (\{i\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{G R i\})))$
20		mapdpglem26.a	$⊢ A = Scalar (U)$
21		mapdpglem26.b	$⊢ B = {Base}_{A}$
22		mapdpglem26.t	$⊢ \underset{˙}{\cdot} = \cdot_{C}$
23		mapdpglem26.o	$⊢ O = 0_{A}$
24		mapdpglem28.ve	$⊢ φ \to v \in B$
25		mapdpglem28.u1	$⊢ φ \to h = u \underset{˙}{\cdot} i$
26		mapdpglem28.u2	$⊢ φ \to G R h = v \underset{˙}{\cdot} (G R i)$
27		mapdpglem28.ue	$⊢ φ \to u \in B$
28		eqid	$⊢ +_{C} = +_{C}$
29		eqid	$⊢ Scalar (C) = Scalar (C)$
30		eqid	$⊢ {Base}_{Scalar (C)} = {Base}_{Scalar (C)}$
31		eqid	$⊢ 0_{C} = 0_{C}$
32	1 8 12	lcdlvec	$⊢ φ \to C \in LVec$
33	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17	mapdpglem30a	$⊢ φ \to G \neq 0_{C}$
34		eldifsn	$⊢ G \in (F ∖ \{0_{C}\}) \leftrightarrow (G \in F \land G \neq 0_{C})$
35	15 33 34	sylanbrc	$⊢ φ \to G \in (F ∖ \{0_{C}\})$
36	19	simpld	$⊢ φ \to i \in F$
37	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19	mapdpglem30b	$⊢ φ \to i \neq 0_{C}$
38		eldifsn	$⊢ i \in (F ∖ \{0_{C}\}) \leftrightarrow (i \in F \land i \neq 0_{C})$
39	36 37 38	sylanbrc	$⊢ φ \to i \in (F ∖ \{0_{C}\})$
40	1 3 20 21 8 29 30 12	lcdsbase	$⊢ φ \to {Base}_{Scalar (C)} = B$
41	24 40	eleqtrrd	$⊢ φ \to v \in {Base}_{Scalar (C)}$
42	1 3 12	dvhlmod	$⊢ φ \to U \in LMod$
43	20	lmodring	$⊢ U \in LMod \to A \in Ring$
44	42 43	syl	$⊢ φ \to A \in Ring$
45		ringgrp	$⊢ A \in Ring \to A \in Grp$
46	44 45	syl	$⊢ φ \to A \in Grp$
47		eqid	$⊢ 1_{A} = 1_{A}$
48	21 47	ringidcl	$⊢ A \in Ring \to 1_{A} \in B$
49	44 48	syl	$⊢ φ \to 1_{A} \in B$
50		eqid	$⊢ {inv}_{g} (A) = {inv}_{g} (A)$
51	21 50	grpinvcl	$⊢ (A \in Grp \land 1_{A} \in B) \to {inv}_{g} (A) (1_{A}) \in B$
52	46 49 51	syl2anc	$⊢ φ \to {inv}_{g} (A) (1_{A}) \in B$
53		eqid	$⊢ \cdot_{A} = \cdot_{A}$
54	21 53	ringcl	$⊢ (A \in Ring \land v \in B \land {inv}_{g} (A) (1_{A}) \in B) \to v \cdot_{A} {inv}_{g} (A) (1_{A}) \in B$
55	44 24 52 54	syl3anc	$⊢ φ \to v \cdot_{A} {inv}_{g} (A) (1_{A}) \in B$
56	55 40	eleqtrrd	$⊢ φ \to v \cdot_{A} {inv}_{g} (A) (1_{A}) \in {Base}_{Scalar (C)}$
57	49 40	eleqtrrd	$⊢ φ \to 1_{A} \in {Base}_{Scalar (C)}$
58	21 53	ringcl	$⊢ (A \in Ring \land u \in B \land {inv}_{g} (A) (1_{A}) \in B) \to u \cdot_{A} {inv}_{g} (A) (1_{A}) \in B$
59	44 27 52 58	syl3anc	$⊢ φ \to u \cdot_{A} {inv}_{g} (A) (1_{A}) \in B$
60	59 40	eleqtrrd	$⊢ φ \to u \cdot_{A} {inv}_{g} (A) (1_{A}) \in {Base}_{Scalar (C)}$
61	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	mapdpglem29	$⊢ φ \to J (\{G\}) \neq J (\{i\})$
62	1 3 20 21 53 8 9 22 12 52 27 36	lcdvsass	$⊢ φ \to (u \cdot_{A} {inv}_{g} (A) (1_{A})) \underset{˙}{\cdot} i = {inv}_{g} (A) (1_{A}) \underset{˙}{\cdot} (u \underset{˙}{\cdot} i)$
63	62	oveq2d	$⊢ φ \to (1_{A} \underset{˙}{\cdot} G) +_{C} ((u \cdot_{A} {inv}_{g} (A) (1_{A})) \underset{˙}{\cdot} i) = (1_{A} \underset{˙}{\cdot} G) +_{C} ({inv}_{g} (A) (1_{A}) \underset{˙}{\cdot} (u \underset{˙}{\cdot} i))$
64	1 3 20 21 8 9 22 12 49 15	lcdvscl	$⊢ φ \to 1_{A} \underset{˙}{\cdot} G \in F$
65	1 3 20 21 8 9 22 12 27 36	lcdvscl	$⊢ φ \to u \underset{˙}{\cdot} i \in F$
66	1 3 20 50 47 8 9 28 22 10 12 64 65	lcdvsub	$⊢ φ \to (1_{A} \underset{˙}{\cdot} G) R (u \underset{˙}{\cdot} i) = (1_{A} \underset{˙}{\cdot} G) +_{C} ({inv}_{g} (A) (1_{A}) \underset{˙}{\cdot} (u \underset{˙}{\cdot} i))$
67	1 3 20 21 53 8 9 22 12 52 24 36	lcdvsass	$⊢ φ \to (v \cdot_{A} {inv}_{g} (A) (1_{A})) \underset{˙}{\cdot} i = {inv}_{g} (A) (1_{A}) \underset{˙}{\cdot} (v \underset{˙}{\cdot} i)$
68	67	oveq2d	$⊢ φ \to (v \underset{˙}{\cdot} G) +_{C} ((v \cdot_{A} {inv}_{g} (A) (1_{A})) \underset{˙}{\cdot} i) = (v \underset{˙}{\cdot} G) +_{C} ({inv}_{g} (A) (1_{A}) \underset{˙}{\cdot} (v \underset{˙}{\cdot} i))$
69	1 3 20 21 8 9 22 12 24 15	lcdvscl	$⊢ φ \to v \underset{˙}{\cdot} G \in F$
70	1 3 20 21 8 9 22 12 24 36	lcdvscl	$⊢ φ \to v \underset{˙}{\cdot} i \in F$
71	1 3 20 50 47 8 9 28 22 10 12 69 70	lcdvsub	$⊢ φ \to (v \underset{˙}{\cdot} G) R (v \underset{˙}{\cdot} i) = (v \underset{˙}{\cdot} G) +_{C} ({inv}_{g} (A) (1_{A}) \underset{˙}{\cdot} (v \underset{˙}{\cdot} i))$
72	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	mapdpglem28	$⊢ φ \to (v \underset{˙}{\cdot} G) R (v \underset{˙}{\cdot} i) = G R (u \underset{˙}{\cdot} i)$
73		eqid	$⊢ 1_{Scalar (C)} = 1_{Scalar (C)}$
74	1 3 20 47 8 29 73 12	lcd1	$⊢ φ \to 1_{Scalar (C)} = 1_{A}$
75	74	oveq1d	$⊢ φ \to 1_{Scalar (C)} \underset{˙}{\cdot} G = 1_{A} \underset{˙}{\cdot} G$
76	1 8 12	lcdlmod	$⊢ φ \to C \in LMod$
77	9 29 22 73	lmodvs1	$⊢ (C \in LMod \land G \in F) \to 1_{Scalar (C)} \underset{˙}{\cdot} G = G$
78	76 15 77	syl2anc	$⊢ φ \to 1_{Scalar (C)} \underset{˙}{\cdot} G = G$
79	75 78	eqtr3d	$⊢ φ \to 1_{A} \underset{˙}{\cdot} G = G$
80	79	oveq1d	$⊢ φ \to (1_{A} \underset{˙}{\cdot} G) R (u \underset{˙}{\cdot} i) = G R (u \underset{˙}{\cdot} i)$
81	72 80	eqtr4d	$⊢ φ \to (v \underset{˙}{\cdot} G) R (v \underset{˙}{\cdot} i) = (1_{A} \underset{˙}{\cdot} G) R (u \underset{˙}{\cdot} i)$
82	68 71 81	3eqtr2rd	$⊢ φ \to (1_{A} \underset{˙}{\cdot} G) R (u \underset{˙}{\cdot} i) = (v \underset{˙}{\cdot} G) +_{C} ((v \cdot_{A} {inv}_{g} (A) (1_{A})) \underset{˙}{\cdot} i)$
83	63 66 82	3eqtr2rd	$⊢ φ \to (v \underset{˙}{\cdot} G) +_{C} ((v \cdot_{A} {inv}_{g} (A) (1_{A})) \underset{˙}{\cdot} i) = (1_{A} \underset{˙}{\cdot} G) +_{C} ((u \cdot_{A} {inv}_{g} (A) (1_{A})) \underset{˙}{\cdot} i)$
84	9 28 29 30 22 31 11 32 35 39 41 56 57 60 61 83	lvecindp2	$⊢ φ \to (v = 1_{A} \land v \cdot_{A} {inv}_{g} (A) (1_{A}) = u \cdot_{A} {inv}_{g} (A) (1_{A}))$
85	21 53 47 50 44 24	rngnegr	$⊢ φ \to v \cdot_{A} {inv}_{g} (A) (1_{A}) = {inv}_{g} (A) (v)$
86	21 53 47 50 44 27	rngnegr	$⊢ φ \to u \cdot_{A} {inv}_{g} (A) (1_{A}) = {inv}_{g} (A) (u)$
87	85 86	eqeq12d	$⊢ φ \to (v \cdot_{A} {inv}_{g} (A) (1_{A}) = u \cdot_{A} {inv}_{g} (A) (1_{A}) \leftrightarrow {inv}_{g} (A) (v) = {inv}_{g} (A) (u))$
88	21 50 46 24 27	grpinv11	$⊢ φ \to ({inv}_{g} (A) (v) = {inv}_{g} (A) (u) \leftrightarrow v = u)$
89	87 88	bitrd	$⊢ φ \to (v \cdot_{A} {inv}_{g} (A) (1_{A}) = u \cdot_{A} {inv}_{g} (A) (1_{A}) \leftrightarrow v = u)$
90	89	anbi2d	$⊢ φ \to ((v = 1_{A} \land v \cdot_{A} {inv}_{g} (A) (1_{A}) = u \cdot_{A} {inv}_{g} (A) (1_{A})) \leftrightarrow (v = 1_{A} \land v = u))$
91	84 90	mpbid	$⊢ φ \to (v = 1_{A} \land v = u)$

Metamath Proof Explorer

Theorem mapdpglem30

Proof