lcfrlem2

	Ref	Expression
Hypotheses	lcfrlem1.v	$⊢ V = {Base}_{U}$
	lcfrlem1.s	$⊢ S = Scalar (U)$
	lcfrlem1.q	$⊢ \underset{˙}{\times} = \cdot_{S}$
	lcfrlem1.z	$⊢ \underset{˙}{0} = 0_{S}$
	lcfrlem1.i	$⊢ I = {inv}_{r} (S)$
	lcfrlem1.f	$⊢ F = LFnl (U)$
	lcfrlem1.d	$⊢ D = LDual (U)$
	lcfrlem1.t	$⊢ \underset{˙}{\cdot} = \cdot_{D}$
	lcfrlem1.m	$⊢ \underset{˙}{-} = -_{D}$
	lcfrlem1.u	$⊢ φ \to U \in LVec$
	lcfrlem1.e	$⊢ φ \to E \in F$
	lcfrlem1.g	$⊢ φ \to G \in F$
	lcfrlem1.x	$⊢ φ \to X \in V$
	lcfrlem1.n	$⊢ φ \to G (X) \neq \underset{˙}{0}$
	lcfrlem1.h	$⊢ H = E \underset{˙}{-} ((I (G (X)) \underset{˙}{\times} E (X)) \underset{˙}{\cdot} G)$
	lcfrlem2.l	$⊢ L = LKer (U)$
Assertion	lcfrlem2	$⊢ φ \to L (E) \cap L (G) \subseteq L (H)$

Proof

Step	Hyp	Ref	Expression
1		lcfrlem1.v	$⊢ V = {Base}_{U}$
2		lcfrlem1.s	$⊢ S = Scalar (U)$
3		lcfrlem1.q	$⊢ \underset{˙}{\times} = \cdot_{S}$
4		lcfrlem1.z	$⊢ \underset{˙}{0} = 0_{S}$
5		lcfrlem1.i	$⊢ I = {inv}_{r} (S)$
6		lcfrlem1.f	$⊢ F = LFnl (U)$
7		lcfrlem1.d	$⊢ D = LDual (U)$
8		lcfrlem1.t	$⊢ \underset{˙}{\cdot} = \cdot_{D}$
9		lcfrlem1.m	$⊢ \underset{˙}{-} = -_{D}$
10		lcfrlem1.u	$⊢ φ \to U \in LVec$
11		lcfrlem1.e	$⊢ φ \to E \in F$
12		lcfrlem1.g	$⊢ φ \to G \in F$
13		lcfrlem1.x	$⊢ φ \to X \in V$
14		lcfrlem1.n	$⊢ φ \to G (X) \neq \underset{˙}{0}$
15		lcfrlem1.h	$⊢ H = E \underset{˙}{-} ((I (G (X)) \underset{˙}{\times} E (X)) \underset{˙}{\cdot} G)$
16		lcfrlem2.l	$⊢ L = LKer (U)$
17		eqid	$⊢ {Base}_{S} = {Base}_{S}$
18		lveclmod	$⊢ U \in LVec \to U \in LMod$
19	10 18	syl	$⊢ φ \to U \in LMod$
20	2	lmodring	$⊢ U \in LMod \to S \in Ring$
21	19 20	syl	$⊢ φ \to S \in Ring$
22	2	lvecdrng	$⊢ U \in LVec \to S \in DivRing$
23	10 22	syl	$⊢ φ \to S \in DivRing$
24	2 17 1 6	lflcl	$⊢ (U \in LVec \land G \in F \land X \in V) \to G (X) \in {Base}_{S}$
25	10 12 13 24	syl3anc	$⊢ φ \to G (X) \in {Base}_{S}$
26	17 4 5	drnginvrcl	$⊢ (S \in DivRing \land G (X) \in {Base}_{S} \land G (X) \neq \underset{˙}{0}) \to I (G (X)) \in {Base}_{S}$
27	23 25 14 26	syl3anc	$⊢ φ \to I (G (X)) \in {Base}_{S}$
28	2 17 1 6	lflcl	$⊢ (U \in LVec \land E \in F \land X \in V) \to E (X) \in {Base}_{S}$
29	10 11 13 28	syl3anc	$⊢ φ \to E (X) \in {Base}_{S}$
30	17 3	ringcl	$⊢ (S \in Ring \land I (G (X)) \in {Base}_{S} \land E (X) \in {Base}_{S}) \to I (G (X)) \underset{˙}{\times} E (X) \in {Base}_{S}$
31	21 27 29 30	syl3anc	$⊢ φ \to I (G (X)) \underset{˙}{\times} E (X) \in {Base}_{S}$
32	2 17 6 16 7 8 10 12 31	lkrss	$⊢ φ \to L (G) \subseteq L ((I (G (X)) \underset{˙}{\times} E (X)) \underset{˙}{\cdot} G)$
33	6 2 17 7 8 19 31 12	ldualvscl	$⊢ φ \to (I (G (X)) \underset{˙}{\times} E (X)) \underset{˙}{\cdot} G \in F$
34		ringgrp	$⊢ S \in Ring \to S \in Grp$
35	21 34	syl	$⊢ φ \to S \in Grp$
36		eqid	$⊢ 1_{S} = 1_{S}$
37	17 36	ringidcl	$⊢ S \in Ring \to 1_{S} \in {Base}_{S}$
38	21 37	syl	$⊢ φ \to 1_{S} \in {Base}_{S}$
39		eqid	$⊢ {inv}_{g} (S) = {inv}_{g} (S)$
40	17 39	grpinvcl	$⊢ (S \in Grp \land 1_{S} \in {Base}_{S}) \to {inv}_{g} (S) (1_{S}) \in {Base}_{S}$
41	35 38 40	syl2anc	$⊢ φ \to {inv}_{g} (S) (1_{S}) \in {Base}_{S}$
42	2 17 6 16 7 8 10 33 41	lkrss	$⊢ φ \to L ((I (G (X)) \underset{˙}{\times} E (X)) \underset{˙}{\cdot} G) \subseteq L ({inv}_{g} (S) (1_{S}) \underset{˙}{\cdot} ((I (G (X)) \underset{˙}{\times} E (X)) \underset{˙}{\cdot} G))$
43	32 42	sstrd	$⊢ φ \to L (G) \subseteq L ({inv}_{g} (S) (1_{S}) \underset{˙}{\cdot} ((I (G (X)) \underset{˙}{\times} E (X)) \underset{˙}{\cdot} G))$
44		sslin	$⊢ L (G) \subseteq L ({inv}_{g} (S) (1_{S}) \underset{˙}{\cdot} ((I (G (X)) \underset{˙}{\times} E (X)) \underset{˙}{\cdot} G)) \to L (E) \cap L (G) \subseteq L (E) \cap L ({inv}_{g} (S) (1_{S}) \underset{˙}{\cdot} ((I (G (X)) \underset{˙}{\times} E (X)) \underset{˙}{\cdot} G))$
45	43 44	syl	$⊢ φ \to L (E) \cap L (G) \subseteq L (E) \cap L ({inv}_{g} (S) (1_{S}) \underset{˙}{\cdot} ((I (G (X)) \underset{˙}{\times} E (X)) \underset{˙}{\cdot} G))$
46		eqid	$⊢ +_{D} = +_{D}$
47	6 2 17 7 8 19 41 33	ldualvscl	$⊢ φ \to {inv}_{g} (S) (1_{S}) \underset{˙}{\cdot} ((I (G (X)) \underset{˙}{\times} E (X)) \underset{˙}{\cdot} G) \in F$
48	6 16 7 46 19 11 47	lkrin	$⊢ φ \to L (E) \cap L ({inv}_{g} (S) (1_{S}) \underset{˙}{\cdot} ((I (G (X)) \underset{˙}{\times} E (X)) \underset{˙}{\cdot} G)) \subseteq L (E +_{D} ({inv}_{g} (S) (1_{S}) \underset{˙}{\cdot} ((I (G (X)) \underset{˙}{\times} E (X)) \underset{˙}{\cdot} G)))$
49	45 48	sstrd	$⊢ φ \to L (E) \cap L (G) \subseteq L (E +_{D} ({inv}_{g} (S) (1_{S}) \underset{˙}{\cdot} ((I (G (X)) \underset{˙}{\times} E (X)) \underset{˙}{\cdot} G)))$
50	15	fveq2i	$⊢ L (H) = L (E \underset{˙}{-} ((I (G (X)) \underset{˙}{\times} E (X)) \underset{˙}{\cdot} G))$
51	2 39 36 6 7 46 8 9 19 11 33	ldualvsub	$⊢ φ \to E \underset{˙}{-} ((I (G (X)) \underset{˙}{\times} E (X)) \underset{˙}{\cdot} G) = E +_{D} ({inv}_{g} (S) (1_{S}) \underset{˙}{\cdot} ((I (G (X)) \underset{˙}{\times} E (X)) \underset{˙}{\cdot} G))$
52	51	fveq2d	$⊢ φ \to L (E \underset{˙}{-} ((I (G (X)) \underset{˙}{\times} E (X)) \underset{˙}{\cdot} G)) = L (E +_{D} ({inv}_{g} (S) (1_{S}) \underset{˙}{\cdot} ((I (G (X)) \underset{˙}{\times} E (X)) \underset{˙}{\cdot} G)))$
53	50 52	syl5req	$⊢ φ \to L (E +_{D} ({inv}_{g} (S) (1_{S}) \underset{˙}{\cdot} ((I (G (X)) \underset{˙}{\times} E (X)) \underset{˙}{\cdot} G))) = L (H)$
54	49 53	sseqtrd	$⊢ φ \to L (E) \cap L (G) \subseteq L (H)$

Metamath Proof Explorer

Theorem lcfrlem2

Proof