lcfl7lem

Description: Lemma for lcfl7N . If two functionals G and J are equal, they are determined by the same vector. (Contributed by NM, 4-Jan-2015)

	Ref	Expression
Hypotheses	lcfl7lem.h	$⊢ H = LHyp (K)$
	lcfl7lem.o	$⊢ \underset{˙}{⊥} = ocH (K) (W)$
	lcfl7lem.u	$⊢ U = DVecH (K) (W)$
	lcfl7lem.v	$⊢ V = {Base}_{U}$
	lcfl7lem.a	$⊢ \underset{˙}{+} = +_{U}$
	lcfl7lem.t	$⊢ \underset{˙}{\cdot} = \cdot_{U}$
	lcfl7lem.s	$⊢ S = Scalar (U)$
	lcfl7lem.r	$⊢ R = {Base}_{S}$
	lcfl7lem.z	$⊢ \underset{˙}{0} = 0_{U}$
	lcfl7lem.f	$⊢ F = LFnl (U)$
	lcfl7lem.l	$⊢ L = LKer (U)$
	lcfl7lem.k	$⊢ φ \to (K \in HL \land W \in H)$
	lcfl7lem.g	$⊢ G = (v \in V ⟼ (ι k \in R \| \exists w \in \underset{˙}{⊥} (\{X\}) v = w \underset{˙}{+} (k \underset{˙}{\cdot} X)))$
	lcfl7lem.j	$⊢ J = (v \in V ⟼ (ι k \in R \| \exists w \in \underset{˙}{⊥} (\{Y\}) v = w \underset{˙}{+} (k \underset{˙}{\cdot} Y)))$
	lcfl7lem.x	$⊢ φ \to X \in (V ∖ \{\underset{˙}{0}\})$
	lcfl7lem.x2	$⊢ φ \to Y \in (V ∖ \{\underset{˙}{0}\})$
	lcfl7lem.gj	$⊢ φ \to G = J$
Assertion	lcfl7lem	$⊢ φ \to X = Y$

Proof

Step	Hyp	Ref	Expression
1		lcfl7lem.h	$⊢ H = LHyp (K)$
2		lcfl7lem.o	$⊢ \underset{˙}{⊥} = ocH (K) (W)$
3		lcfl7lem.u	$⊢ U = DVecH (K) (W)$
4		lcfl7lem.v	$⊢ V = {Base}_{U}$
5		lcfl7lem.a	$⊢ \underset{˙}{+} = +_{U}$
6		lcfl7lem.t	$⊢ \underset{˙}{\cdot} = \cdot_{U}$
7		lcfl7lem.s	$⊢ S = Scalar (U)$
8		lcfl7lem.r	$⊢ R = {Base}_{S}$
9		lcfl7lem.z	$⊢ \underset{˙}{0} = 0_{U}$
10		lcfl7lem.f	$⊢ F = LFnl (U)$
11		lcfl7lem.l	$⊢ L = LKer (U)$
12		lcfl7lem.k	$⊢ φ \to (K \in HL \land W \in H)$
13		lcfl7lem.g	$⊢ G = (v \in V ⟼ (ι k \in R \| \exists w \in \underset{˙}{⊥} (\{X\}) v = w \underset{˙}{+} (k \underset{˙}{\cdot} X)))$
14		lcfl7lem.j	$⊢ J = (v \in V ⟼ (ι k \in R \| \exists w \in \underset{˙}{⊥} (\{Y\}) v = w \underset{˙}{+} (k \underset{˙}{\cdot} Y)))$
15		lcfl7lem.x	$⊢ φ \to X \in (V ∖ \{\underset{˙}{0}\})$
16		lcfl7lem.x2	$⊢ φ \to Y \in (V ∖ \{\underset{˙}{0}\})$
17		lcfl7lem.gj	$⊢ φ \to G = J$
18	1 2 3 4 9 5 6 11 7 8 13 12 15	dochsnkr2cl	$⊢ φ \to X \in (\underset{˙}{⊥} (L (G)) ∖ \{\underset{˙}{0}\})$
19	18	eldifad	$⊢ φ \to X \in \underset{˙}{⊥} (L (G))$
20	17	fveq2d	$⊢ φ \to L (G) = L (J)$
21	1 2 3 4 9 5 6 11 7 8 14 12 16	dochsnkr2	$⊢ φ \to L (J) = \underset{˙}{⊥} (\{Y\})$
22	20 21	eqtrd	$⊢ φ \to L (G) = \underset{˙}{⊥} (\{Y\})$
23	22	fveq2d	$⊢ φ \to \underset{˙}{⊥} (L (G)) = \underset{˙}{⊥} (\underset{˙}{⊥} (\{Y\}))$
24		eqid	$⊢ LSpan (U) = LSpan (U)$
25	16	eldifad	$⊢ φ \to Y \in V$
26	25	snssd	$⊢ φ \to \{Y\} \subseteq V$
27	1 3 2 4 24 12 26	dochocsp	$⊢ φ \to \underset{˙}{⊥} (LSpan (U) (\{Y\})) = \underset{˙}{⊥} (\{Y\})$
28	27	fveq2d	$⊢ φ \to \underset{˙}{⊥} (\underset{˙}{⊥} (LSpan (U) (\{Y\}))) = \underset{˙}{⊥} (\underset{˙}{⊥} (\{Y\}))$
29		eqid	$⊢ DIsoH (K) (W) = DIsoH (K) (W)$
30	1 3 4 24 29	dihlsprn	$⊢ ((K \in HL \land W \in H) \land Y \in V) \to LSpan (U) (\{Y\}) \in ran DIsoH (K) (W)$
31	12 25 30	syl2anc	$⊢ φ \to LSpan (U) (\{Y\}) \in ran DIsoH (K) (W)$
32	1 29 2	dochoc	$⊢ ((K \in HL \land W \in H) \land LSpan (U) (\{Y\}) \in ran DIsoH (K) (W)) \to \underset{˙}{⊥} (\underset{˙}{⊥} (LSpan (U) (\{Y\}))) = LSpan (U) (\{Y\})$
33	12 31 32	syl2anc	$⊢ φ \to \underset{˙}{⊥} (\underset{˙}{⊥} (LSpan (U) (\{Y\}))) = LSpan (U) (\{Y\})$
34	23 28 33	3eqtr2d	$⊢ φ \to \underset{˙}{⊥} (L (G)) = LSpan (U) (\{Y\})$
35	19 34	eleqtrd	$⊢ φ \to X \in LSpan (U) (\{Y\})$
36	1 3 12	dvhlmod	$⊢ φ \to U \in LMod$
37	7 8 4 6 24	lspsnel	$⊢ (U \in LMod \land Y \in V) \to (X \in LSpan (U) (\{Y\}) \leftrightarrow \exists s \in R X = s \underset{˙}{\cdot} Y)$
38	36 25 37	syl2anc	$⊢ φ \to (X \in LSpan (U) (\{Y\}) \leftrightarrow \exists s \in R X = s \underset{˙}{\cdot} Y)$
39	35 38	mpbid	$⊢ φ \to \exists s \in R X = s \underset{˙}{\cdot} Y$
40		simp3	$⊢ (φ \land s \in R \land X = s \underset{˙}{\cdot} Y) \to X = s \underset{˙}{\cdot} Y$
41		fveq2	$⊢ X = s \underset{˙}{\cdot} Y \to G (X) = G (s \underset{˙}{\cdot} Y)$
42	41	3ad2ant3	$⊢ (φ \land s \in R \land X = s \underset{˙}{\cdot} Y) \to G (X) = G (s \underset{˙}{\cdot} Y)$
43		eqid	$⊢ 1_{S} = 1_{S}$
44	1 2 3 4 5 6 9 7 8 43 12 16 14	dochfl1	$⊢ φ \to J (Y) = 1_{S}$
45	17	fveq1d	$⊢ φ \to G (Y) = J (Y)$
46	1 2 3 4 5 6 9 7 8 43 12 15 13	dochfl1	$⊢ φ \to G (X) = 1_{S}$
47	44 45 46	3eqtr4rd	$⊢ φ \to G (X) = G (Y)$
48	47	3ad2ant1	$⊢ (φ \land s \in R \land X = s \underset{˙}{\cdot} Y) \to G (X) = G (Y)$
49	36	3ad2ant1	$⊢ (φ \land s \in R \land X = s \underset{˙}{\cdot} Y) \to U \in LMod$
50	1 2 3 4 9 5 6 10 7 8 13 12 15	dochflcl	$⊢ φ \to G \in F$
51	50	3ad2ant1	$⊢ (φ \land s \in R \land X = s \underset{˙}{\cdot} Y) \to G \in F$
52		simp2	$⊢ (φ \land s \in R \land X = s \underset{˙}{\cdot} Y) \to s \in R$
53	25	3ad2ant1	$⊢ (φ \land s \in R \land X = s \underset{˙}{\cdot} Y) \to Y \in V$
54		eqid	$⊢ \cdot_{S} = \cdot_{S}$
55	7 8 54 4 6 10	lflmul	$⊢ (U \in LMod \land G \in F \land (s \in R \land Y \in V)) \to G (s \underset{˙}{\cdot} Y) = s \cdot_{S} G (Y)$
56	49 51 52 53 55	syl112anc	$⊢ (φ \land s \in R \land X = s \underset{˙}{\cdot} Y) \to G (s \underset{˙}{\cdot} Y) = s \cdot_{S} G (Y)$
57	42 48 56	3eqtr3d	$⊢ (φ \land s \in R \land X = s \underset{˙}{\cdot} Y) \to G (Y) = s \cdot_{S} G (Y)$
58	57	oveq1d	$⊢ (φ \land s \in R \land X = s \underset{˙}{\cdot} Y) \to G (Y) \cdot_{S} {inv}_{r} (S) (G (Y)) = (s \cdot_{S} G (Y)) \cdot_{S} {inv}_{r} (S) (G (Y))$
59	7	lmodring	$⊢ U \in LMod \to S \in Ring$
60	36 59	syl	$⊢ φ \to S \in Ring$
61	60	3ad2ant1	$⊢ (φ \land s \in R \land X = s \underset{˙}{\cdot} Y) \to S \in Ring$
62	7 8 4 10	lflcl	$⊢ (U \in LMod \land G \in F \land Y \in V) \to G (Y) \in R$
63	36 50 25 62	syl3anc	$⊢ φ \to G (Y) \in R$
64	63	3ad2ant1	$⊢ (φ \land s \in R \land X = s \underset{˙}{\cdot} Y) \to G (Y) \in R$
65	1 3 12	dvhlvec	$⊢ φ \to U \in LVec$
66	7	lvecdrng	$⊢ U \in LVec \to S \in DivRing$
67	65 66	syl	$⊢ φ \to S \in DivRing$
68	45 44	eqtrd	$⊢ φ \to G (Y) = 1_{S}$
69		eqid	$⊢ 0_{S} = 0_{S}$
70	69 43	drngunz	$⊢ S \in DivRing \to 1_{S} \neq 0_{S}$
71	67 70	syl	$⊢ φ \to 1_{S} \neq 0_{S}$
72	68 71	eqnetrd	$⊢ φ \to G (Y) \neq 0_{S}$
73		eqid	$⊢ {inv}_{r} (S) = {inv}_{r} (S)$
74	8 69 73	drnginvrcl	$⊢ (S \in DivRing \land G (Y) \in R \land G (Y) \neq 0_{S}) \to {inv}_{r} (S) (G (Y)) \in R$
75	67 63 72 74	syl3anc	$⊢ φ \to {inv}_{r} (S) (G (Y)) \in R$
76	75	3ad2ant1	$⊢ (φ \land s \in R \land X = s \underset{˙}{\cdot} Y) \to {inv}_{r} (S) (G (Y)) \in R$
77	8 54	ringass	$⊢ (S \in Ring \land (s \in R \land G (Y) \in R \land {inv}_{r} (S) (G (Y)) \in R)) \to (s \cdot_{S} G (Y)) \cdot_{S} {inv}_{r} (S) (G (Y)) = s \cdot_{S} (G (Y) \cdot_{S} {inv}_{r} (S) (G (Y)))$
78	61 52 64 76 77	syl13anc	$⊢ (φ \land s \in R \land X = s \underset{˙}{\cdot} Y) \to (s \cdot_{S} G (Y)) \cdot_{S} {inv}_{r} (S) (G (Y)) = s \cdot_{S} (G (Y) \cdot_{S} {inv}_{r} (S) (G (Y)))$
79	8 69 54 43 73	drnginvrr	$⊢ (S \in DivRing \land G (Y) \in R \land G (Y) \neq 0_{S}) \to G (Y) \cdot_{S} {inv}_{r} (S) (G (Y)) = 1_{S}$
80	67 63 72 79	syl3anc	$⊢ φ \to G (Y) \cdot_{S} {inv}_{r} (S) (G (Y)) = 1_{S}$
81	80	3ad2ant1	$⊢ (φ \land s \in R \land X = s \underset{˙}{\cdot} Y) \to G (Y) \cdot_{S} {inv}_{r} (S) (G (Y)) = 1_{S}$
82	81	oveq2d	$⊢ (φ \land s \in R \land X = s \underset{˙}{\cdot} Y) \to s \cdot_{S} (G (Y) \cdot_{S} {inv}_{r} (S) (G (Y))) = s \cdot_{S} 1_{S}$
83	58 78 82	3eqtrrd	$⊢ (φ \land s \in R \land X = s \underset{˙}{\cdot} Y) \to s \cdot_{S} 1_{S} = G (Y) \cdot_{S} {inv}_{r} (S) (G (Y))$
84	8 54 43	ringridm	$⊢ (S \in Ring \land s \in R) \to s \cdot_{S} 1_{S} = s$
85	61 52 84	syl2anc	$⊢ (φ \land s \in R \land X = s \underset{˙}{\cdot} Y) \to s \cdot_{S} 1_{S} = s$
86	83 85 81	3eqtr3d	$⊢ (φ \land s \in R \land X = s \underset{˙}{\cdot} Y) \to s = 1_{S}$
87		oveq1	$⊢ s = 1_{S} \to s \underset{˙}{\cdot} Y = 1_{S} \underset{˙}{\cdot} Y$
88	4 7 6 43	lmodvs1	$⊢ (U \in LMod \land Y \in V) \to 1_{S} \underset{˙}{\cdot} Y = Y$
89	36 25 88	syl2anc	$⊢ φ \to 1_{S} \underset{˙}{\cdot} Y = Y$
90	89	3ad2ant1	$⊢ (φ \land s \in R \land X = s \underset{˙}{\cdot} Y) \to 1_{S} \underset{˙}{\cdot} Y = Y$
91	87 90	sylan9eqr	$⊢ ((φ \land s \in R \land X = s \underset{˙}{\cdot} Y) \land s = 1_{S}) \to s \underset{˙}{\cdot} Y = Y$
92	86 91	mpdan	$⊢ (φ \land s \in R \land X = s \underset{˙}{\cdot} Y) \to s \underset{˙}{\cdot} Y = Y$
93	40 92	eqtrd	$⊢ (φ \land s \in R \land X = s \underset{˙}{\cdot} Y) \to X = Y$
94	93	rexlimdv3a	$⊢ φ \to (\exists s \in R X = s \underset{˙}{\cdot} Y \to X = Y)$
95	39 94	mpd	$⊢ φ \to X = Y$

Metamath Proof Explorer

Theorem lcfl7lem

Proof