lclkrlem2m

Description: Lemma for lclkr . Construct a vector B that makes the sum of functionals zero. Combine with B e. V to shorten overall proof. (Contributed by NM, 17-Jan-2015)

	Ref	Expression
Hypotheses	lclkrlem2m.v	$⊢ V = {Base}_{U}$
	lclkrlem2m.t	$⊢ \underset{˙}{\cdot} = \cdot_{U}$
	lclkrlem2m.s	$⊢ S = Scalar (U)$
	lclkrlem2m.q	$⊢ \underset{˙}{\times} = \cdot_{S}$
	lclkrlem2m.z	$⊢ \underset{˙}{0} = 0_{S}$
	lclkrlem2m.i	$⊢ I = {inv}_{r} (S)$
	lclkrlem2m.m	$⊢ \underset{˙}{-} = -_{U}$
	lclkrlem2m.f	$⊢ F = LFnl (U)$
	lclkrlem2m.d	$⊢ D = LDual (U)$
	lclkrlem2m.p	$⊢ \underset{˙}{+} = +_{D}$
	lclkrlem2m.x	$⊢ φ \to X \in V$
	lclkrlem2m.y	$⊢ φ \to Y \in V$
	lclkrlem2m.e	$⊢ φ \to E \in F$
	lclkrlem2m.g	$⊢ φ \to G \in F$
	lclkrlem2m.w	$⊢ φ \to U \in LVec$
	lclkrlem2m.b	$⊢ B = X \underset{˙}{-} (((E \underset{˙}{+} G) (X) \underset{˙}{\times} I ((E \underset{˙}{+} G) (Y))) \underset{˙}{\cdot} Y)$
	lclkrlem2m.n	$⊢ φ \to (E \underset{˙}{+} G) (Y) \neq \underset{˙}{0}$
Assertion	lclkrlem2m	$⊢ φ \to (B \in V \land (E \underset{˙}{+} G) (B) = \underset{˙}{0})$

Proof

Step	Hyp	Ref	Expression
1		lclkrlem2m.v	$⊢ V = {Base}_{U}$
2		lclkrlem2m.t	$⊢ \underset{˙}{\cdot} = \cdot_{U}$
3		lclkrlem2m.s	$⊢ S = Scalar (U)$
4		lclkrlem2m.q	$⊢ \underset{˙}{\times} = \cdot_{S}$
5		lclkrlem2m.z	$⊢ \underset{˙}{0} = 0_{S}$
6		lclkrlem2m.i	$⊢ I = {inv}_{r} (S)$
7		lclkrlem2m.m	$⊢ \underset{˙}{-} = -_{U}$
8		lclkrlem2m.f	$⊢ F = LFnl (U)$
9		lclkrlem2m.d	$⊢ D = LDual (U)$
10		lclkrlem2m.p	$⊢ \underset{˙}{+} = +_{D}$
11		lclkrlem2m.x	$⊢ φ \to X \in V$
12		lclkrlem2m.y	$⊢ φ \to Y \in V$
13		lclkrlem2m.e	$⊢ φ \to E \in F$
14		lclkrlem2m.g	$⊢ φ \to G \in F$
15		lclkrlem2m.w	$⊢ φ \to U \in LVec$
16		lclkrlem2m.b	$⊢ B = X \underset{˙}{-} (((E \underset{˙}{+} G) (X) \underset{˙}{\times} I ((E \underset{˙}{+} G) (Y))) \underset{˙}{\cdot} Y)$
17		lclkrlem2m.n	$⊢ φ \to (E \underset{˙}{+} G) (Y) \neq \underset{˙}{0}$
18		lveclmod	$⊢ U \in LVec \to U \in LMod$
19	15 18	syl	$⊢ φ \to U \in LMod$
20		lmodgrp	$⊢ U \in LMod \to U \in Grp$
21	19 20	syl	$⊢ φ \to U \in Grp$
22	3	lmodring	$⊢ U \in LMod \to S \in Ring$
23	19 22	syl	$⊢ φ \to S \in Ring$
24	8 9 10 19 13 14	ldualvaddcl	$⊢ φ \to E \underset{˙}{+} G \in F$
25		eqid	$⊢ {Base}_{S} = {Base}_{S}$
26	3 25 1 8	lflcl	$⊢ (U \in LVec \land E \underset{˙}{+} G \in F \land X \in V) \to (E \underset{˙}{+} G) (X) \in {Base}_{S}$
27	15 24 11 26	syl3anc	$⊢ φ \to (E \underset{˙}{+} G) (X) \in {Base}_{S}$
28	3	lvecdrng	$⊢ U \in LVec \to S \in DivRing$
29	15 28	syl	$⊢ φ \to S \in DivRing$
30	3 25 1 8	lflcl	$⊢ (U \in LVec \land E \underset{˙}{+} G \in F \land Y \in V) \to (E \underset{˙}{+} G) (Y) \in {Base}_{S}$
31	15 24 12 30	syl3anc	$⊢ φ \to (E \underset{˙}{+} G) (Y) \in {Base}_{S}$
32	25 5 6	drnginvrcl	$⊢ (S \in DivRing \land (E \underset{˙}{+} G) (Y) \in {Base}_{S} \land (E \underset{˙}{+} G) (Y) \neq \underset{˙}{0}) \to I ((E \underset{˙}{+} G) (Y)) \in {Base}_{S}$
33	29 31 17 32	syl3anc	$⊢ φ \to I ((E \underset{˙}{+} G) (Y)) \in {Base}_{S}$
34	25 4	ringcl	$⊢ (S \in Ring \land (E \underset{˙}{+} G) (X) \in {Base}_{S} \land I ((E \underset{˙}{+} G) (Y)) \in {Base}_{S}) \to (E \underset{˙}{+} G) (X) \underset{˙}{\times} I ((E \underset{˙}{+} G) (Y)) \in {Base}_{S}$
35	23 27 33 34	syl3anc	$⊢ φ \to (E \underset{˙}{+} G) (X) \underset{˙}{\times} I ((E \underset{˙}{+} G) (Y)) \in {Base}_{S}$
36	1 3 2 25	lmodvscl	$⊢ (U \in LMod \land (E \underset{˙}{+} G) (X) \underset{˙}{\times} I ((E \underset{˙}{+} G) (Y)) \in {Base}_{S} \land Y \in V) \to ((E \underset{˙}{+} G) (X) \underset{˙}{\times} I ((E \underset{˙}{+} G) (Y))) \underset{˙}{\cdot} Y \in V$
37	19 35 12 36	syl3anc	$⊢ φ \to ((E \underset{˙}{+} G) (X) \underset{˙}{\times} I ((E \underset{˙}{+} G) (Y))) \underset{˙}{\cdot} Y \in V$
38	1 7	grpsubcl	$⊢ (U \in Grp \land X \in V \land ((E \underset{˙}{+} G) (X) \underset{˙}{\times} I ((E \underset{˙}{+} G) (Y))) \underset{˙}{\cdot} Y \in V) \to X \underset{˙}{-} (((E \underset{˙}{+} G) (X) \underset{˙}{\times} I ((E \underset{˙}{+} G) (Y))) \underset{˙}{\cdot} Y) \in V$
39	21 11 37 38	syl3anc	$⊢ φ \to X \underset{˙}{-} (((E \underset{˙}{+} G) (X) \underset{˙}{\times} I ((E \underset{˙}{+} G) (Y))) \underset{˙}{\cdot} Y) \in V$
40	16 39	eqeltrid	$⊢ φ \to B \in V$
41	16	fveq2i	$⊢ (E \underset{˙}{+} G) (B) = (E \underset{˙}{+} G) (X \underset{˙}{-} (((E \underset{˙}{+} G) (X) \underset{˙}{\times} I ((E \underset{˙}{+} G) (Y))) \underset{˙}{\cdot} Y))$
42		eqid	$⊢ -_{S} = -_{S}$
43	3 42 1 7 8	lflsub	$⊢ (U \in LMod \land E \underset{˙}{+} G \in F \land (X \in V \land ((E \underset{˙}{+} G) (X) \underset{˙}{\times} I ((E \underset{˙}{+} G) (Y))) \underset{˙}{\cdot} Y \in V)) \to (E \underset{˙}{+} G) (X \underset{˙}{-} (((E \underset{˙}{+} G) (X) \underset{˙}{\times} I ((E \underset{˙}{+} G) (Y))) \underset{˙}{\cdot} Y)) = (E \underset{˙}{+} G) (X) -_{S} (E \underset{˙}{+} G) (((E \underset{˙}{+} G) (X) \underset{˙}{\times} I ((E \underset{˙}{+} G) (Y))) \underset{˙}{\cdot} Y)$
44	19 24 11 37 43	syl112anc	$⊢ φ \to (E \underset{˙}{+} G) (X \underset{˙}{-} (((E \underset{˙}{+} G) (X) \underset{˙}{\times} I ((E \underset{˙}{+} G) (Y))) \underset{˙}{\cdot} Y)) = (E \underset{˙}{+} G) (X) -_{S} (E \underset{˙}{+} G) (((E \underset{˙}{+} G) (X) \underset{˙}{\times} I ((E \underset{˙}{+} G) (Y))) \underset{˙}{\cdot} Y)$
45	3 25 4 1 2 8	lflmul	$⊢ (U \in LMod \land E \underset{˙}{+} G \in F \land ((E \underset{˙}{+} G) (X) \underset{˙}{\times} I ((E \underset{˙}{+} G) (Y)) \in {Base}_{S} \land Y \in V)) \to (E \underset{˙}{+} G) (((E \underset{˙}{+} G) (X) \underset{˙}{\times} I ((E \underset{˙}{+} G) (Y))) \underset{˙}{\cdot} Y) = ((E \underset{˙}{+} G) (X) \underset{˙}{\times} I ((E \underset{˙}{+} G) (Y))) \underset{˙}{\times} (E \underset{˙}{+} G) (Y)$
46	19 24 35 12 45	syl112anc	$⊢ φ \to (E \underset{˙}{+} G) (((E \underset{˙}{+} G) (X) \underset{˙}{\times} I ((E \underset{˙}{+} G) (Y))) \underset{˙}{\cdot} Y) = ((E \underset{˙}{+} G) (X) \underset{˙}{\times} I ((E \underset{˙}{+} G) (Y))) \underset{˙}{\times} (E \underset{˙}{+} G) (Y)$
47	25 4	ringass	$⊢ (S \in Ring \land ((E \underset{˙}{+} G) (X) \in {Base}_{S} \land I ((E \underset{˙}{+} G) (Y)) \in {Base}_{S} \land (E \underset{˙}{+} G) (Y) \in {Base}_{S})) \to ((E \underset{˙}{+} G) (X) \underset{˙}{\times} I ((E \underset{˙}{+} G) (Y))) \underset{˙}{\times} (E \underset{˙}{+} G) (Y) = (E \underset{˙}{+} G) (X) \underset{˙}{\times} (I ((E \underset{˙}{+} G) (Y)) \underset{˙}{\times} (E \underset{˙}{+} G) (Y))$
48	23 27 33 31 47	syl13anc	$⊢ φ \to ((E \underset{˙}{+} G) (X) \underset{˙}{\times} I ((E \underset{˙}{+} G) (Y))) \underset{˙}{\times} (E \underset{˙}{+} G) (Y) = (E \underset{˙}{+} G) (X) \underset{˙}{\times} (I ((E \underset{˙}{+} G) (Y)) \underset{˙}{\times} (E \underset{˙}{+} G) (Y))$
49		eqid	$⊢ 1_{S} = 1_{S}$
50	25 5 4 49 6	drnginvrl	$⊢ (S \in DivRing \land (E \underset{˙}{+} G) (Y) \in {Base}_{S} \land (E \underset{˙}{+} G) (Y) \neq \underset{˙}{0}) \to I ((E \underset{˙}{+} G) (Y)) \underset{˙}{\times} (E \underset{˙}{+} G) (Y) = 1_{S}$
51	29 31 17 50	syl3anc	$⊢ φ \to I ((E \underset{˙}{+} G) (Y)) \underset{˙}{\times} (E \underset{˙}{+} G) (Y) = 1_{S}$
52	51	oveq2d	$⊢ φ \to (E \underset{˙}{+} G) (X) \underset{˙}{\times} (I ((E \underset{˙}{+} G) (Y)) \underset{˙}{\times} (E \underset{˙}{+} G) (Y)) = (E \underset{˙}{+} G) (X) \underset{˙}{\times} 1_{S}$
53	48 52	eqtrd	$⊢ φ \to ((E \underset{˙}{+} G) (X) \underset{˙}{\times} I ((E \underset{˙}{+} G) (Y))) \underset{˙}{\times} (E \underset{˙}{+} G) (Y) = (E \underset{˙}{+} G) (X) \underset{˙}{\times} 1_{S}$
54	25 4 49	ringridm	$⊢ (S \in Ring \land (E \underset{˙}{+} G) (X) \in {Base}_{S}) \to (E \underset{˙}{+} G) (X) \underset{˙}{\times} 1_{S} = (E \underset{˙}{+} G) (X)$
55	23 27 54	syl2anc	$⊢ φ \to (E \underset{˙}{+} G) (X) \underset{˙}{\times} 1_{S} = (E \underset{˙}{+} G) (X)$
56	46 53 55	3eqtrd	$⊢ φ \to (E \underset{˙}{+} G) (((E \underset{˙}{+} G) (X) \underset{˙}{\times} I ((E \underset{˙}{+} G) (Y))) \underset{˙}{\cdot} Y) = (E \underset{˙}{+} G) (X)$
57	56	oveq2d	$⊢ φ \to (E \underset{˙}{+} G) (X) -_{S} (E \underset{˙}{+} G) (((E \underset{˙}{+} G) (X) \underset{˙}{\times} I ((E \underset{˙}{+} G) (Y))) \underset{˙}{\cdot} Y) = (E \underset{˙}{+} G) (X) -_{S} (E \underset{˙}{+} G) (X)$
58		ringgrp	$⊢ S \in Ring \to S \in Grp$
59	23 58	syl	$⊢ φ \to S \in Grp$
60	25 5 42	grpsubid	$⊢ (S \in Grp \land (E \underset{˙}{+} G) (X) \in {Base}_{S}) \to (E \underset{˙}{+} G) (X) -_{S} (E \underset{˙}{+} G) (X) = \underset{˙}{0}$
61	59 27 60	syl2anc	$⊢ φ \to (E \underset{˙}{+} G) (X) -_{S} (E \underset{˙}{+} G) (X) = \underset{˙}{0}$
62	44 57 61	3eqtrd	$⊢ φ \to (E \underset{˙}{+} G) (X \underset{˙}{-} (((E \underset{˙}{+} G) (X) \underset{˙}{\times} I ((E \underset{˙}{+} G) (Y))) \underset{˙}{\cdot} Y)) = \underset{˙}{0}$
63	41 62	syl5eq	$⊢ φ \to (E \underset{˙}{+} G) (B) = \underset{˙}{0}$
64	40 63	jca	$⊢ φ \to (B \in V \land (E \underset{˙}{+} G) (B) = \underset{˙}{0})$

Metamath Proof Explorer

Theorem lclkrlem2m

Proof