Theorem lcfrlem2

Description: Lemma for lcfr . (Contributed by NM, 27-Feb-2015)

	Ref	Expression
Hypotheses	lcfrlem1.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
	lcfrlem1.s	⊢ 𝑆 = ( Scalar ‘ 𝑈 )
	lcfrlem1.q	⊢ × = ( .r ‘ 𝑆 )
	lcfrlem1.z	⊢ 0 = ( 0g ‘ 𝑆 )
	lcfrlem1.i	⊢ 𝐼 = ( invr ‘ 𝑆 )
	lcfrlem1.f	⊢ 𝐹 = ( LFnl ‘ 𝑈 )
	lcfrlem1.d	⊢ 𝐷 = ( LDual ‘ 𝑈 )
	lcfrlem1.t	⊢ · = ( ·𝑠 ‘ 𝐷 )
	lcfrlem1.m	⊢ − = ( -g ‘ 𝐷 )
	lcfrlem1.u	⊢ ( 𝜑 → 𝑈 ∈ LVec )
	lcfrlem1.e	⊢ ( 𝜑 → 𝐸 ∈ 𝐹 )
	lcfrlem1.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
	lcfrlem1.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
	lcfrlem1.n	⊢ ( 𝜑 → ( 𝐺 ‘ 𝑋 ) ≠ 0 )
	lcfrlem1.h	⊢ 𝐻 = ( 𝐸 − ( ( ( 𝐼 ‘ ( 𝐺 ‘ 𝑋 ) ) × ( 𝐸 ‘ 𝑋 ) ) · 𝐺 ) )
	lcfrlem2.l	⊢ 𝐿 = ( LKer ‘ 𝑈 )
Assertion	lcfrlem2	⊢ ( 𝜑 → ( ( 𝐿 ‘ 𝐸 ) ∩ ( 𝐿 ‘ 𝐺 ) ) ⊆ ( 𝐿 ‘ 𝐻 ) )

Proof

Step	Hyp	Ref	Expression
1		lcfrlem1.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
2		lcfrlem1.s	⊢ 𝑆 = ( Scalar ‘ 𝑈 )
3		lcfrlem1.q	⊢ × = ( .r ‘ 𝑆 )
4		lcfrlem1.z	⊢ 0 = ( 0g ‘ 𝑆 )
5		lcfrlem1.i	⊢ 𝐼 = ( invr ‘ 𝑆 )
6		lcfrlem1.f	⊢ 𝐹 = ( LFnl ‘ 𝑈 )
7		lcfrlem1.d	⊢ 𝐷 = ( LDual ‘ 𝑈 )
8		lcfrlem1.t	⊢ · = ( ·𝑠 ‘ 𝐷 )
9		lcfrlem1.m	⊢ − = ( -g ‘ 𝐷 )
10		lcfrlem1.u	⊢ ( 𝜑 → 𝑈 ∈ LVec )
11		lcfrlem1.e	⊢ ( 𝜑 → 𝐸 ∈ 𝐹 )
12		lcfrlem1.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
13		lcfrlem1.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
14		lcfrlem1.n	⊢ ( 𝜑 → ( 𝐺 ‘ 𝑋 ) ≠ 0 )
15		lcfrlem1.h	⊢ 𝐻 = ( 𝐸 − ( ( ( 𝐼 ‘ ( 𝐺 ‘ 𝑋 ) ) × ( 𝐸 ‘ 𝑋 ) ) · 𝐺 ) )
16		lcfrlem2.l	⊢ 𝐿 = ( LKer ‘ 𝑈 )
17		eqid	⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
18		lveclmod	⊢ ( 𝑈 ∈ LVec → 𝑈 ∈ LMod )
19	10 18	syl	⊢ ( 𝜑 → 𝑈 ∈ LMod )
20	2	lmodring	⊢ ( 𝑈 ∈ LMod → 𝑆 ∈ Ring )
21	19 20	syl	⊢ ( 𝜑 → 𝑆 ∈ Ring )
22	2	lvecdrng	⊢ ( 𝑈 ∈ LVec → 𝑆 ∈ DivRing )
23	10 22	syl	⊢ ( 𝜑 → 𝑆 ∈ DivRing )
24	2 17 1 6	lflcl	⊢ ( ( 𝑈 ∈ LVec ∧ 𝐺 ∈ 𝐹 ∧ 𝑋 ∈ 𝑉 ) → ( 𝐺 ‘ 𝑋 ) ∈ ( Base ‘ 𝑆 ) )
25	10 12 13 24	syl3anc	⊢ ( 𝜑 → ( 𝐺 ‘ 𝑋 ) ∈ ( Base ‘ 𝑆 ) )
26	17 4 5	drnginvrcl	⊢ ( ( 𝑆 ∈ DivRing ∧ ( 𝐺 ‘ 𝑋 ) ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐺 ‘ 𝑋 ) ≠ 0 ) → ( 𝐼 ‘ ( 𝐺 ‘ 𝑋 ) ) ∈ ( Base ‘ 𝑆 ) )
27	23 25 14 26	syl3anc	⊢ ( 𝜑 → ( 𝐼 ‘ ( 𝐺 ‘ 𝑋 ) ) ∈ ( Base ‘ 𝑆 ) )
28	2 17 1 6	lflcl	⊢ ( ( 𝑈 ∈ LVec ∧ 𝐸 ∈ 𝐹 ∧ 𝑋 ∈ 𝑉 ) → ( 𝐸 ‘ 𝑋 ) ∈ ( Base ‘ 𝑆 ) )
29	10 11 13 28	syl3anc	⊢ ( 𝜑 → ( 𝐸 ‘ 𝑋 ) ∈ ( Base ‘ 𝑆 ) )
30	17 3	ringcl	⊢ ( ( 𝑆 ∈ Ring ∧ ( 𝐼 ‘ ( 𝐺 ‘ 𝑋 ) ) ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐸 ‘ 𝑋 ) ∈ ( Base ‘ 𝑆 ) ) → ( ( 𝐼 ‘ ( 𝐺 ‘ 𝑋 ) ) × ( 𝐸 ‘ 𝑋 ) ) ∈ ( Base ‘ 𝑆 ) )
31	21 27 29 30	syl3anc	⊢ ( 𝜑 → ( ( 𝐼 ‘ ( 𝐺 ‘ 𝑋 ) ) × ( 𝐸 ‘ 𝑋 ) ) ∈ ( Base ‘ 𝑆 ) )
32	2 17 6 16 7 8 10 12 31	lkrss	⊢ ( 𝜑 → ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ ( ( ( 𝐼 ‘ ( 𝐺 ‘ 𝑋 ) ) × ( 𝐸 ‘ 𝑋 ) ) · 𝐺 ) ) )
33	6 2 17 7 8 19 31 12	ldualvscl	⊢ ( 𝜑 → ( ( ( 𝐼 ‘ ( 𝐺 ‘ 𝑋 ) ) × ( 𝐸 ‘ 𝑋 ) ) · 𝐺 ) ∈ 𝐹 )
34		ringgrp	⊢ ( 𝑆 ∈ Ring → 𝑆 ∈ Grp )
35	21 34	syl	⊢ ( 𝜑 → 𝑆 ∈ Grp )
36		eqid	⊢ ( 1r ‘ 𝑆 ) = ( 1r ‘ 𝑆 )
37	17 36	ringidcl	⊢ ( 𝑆 ∈ Ring → ( 1r ‘ 𝑆 ) ∈ ( Base ‘ 𝑆 ) )
38	21 37	syl	⊢ ( 𝜑 → ( 1r ‘ 𝑆 ) ∈ ( Base ‘ 𝑆 ) )
39		eqid	⊢ ( invg ‘ 𝑆 ) = ( invg ‘ 𝑆 )
40	17 39	grpinvcl	⊢ ( ( 𝑆 ∈ Grp ∧ ( 1r ‘ 𝑆 ) ∈ ( Base ‘ 𝑆 ) ) → ( ( invg ‘ 𝑆 ) ‘ ( 1r ‘ 𝑆 ) ) ∈ ( Base ‘ 𝑆 ) )
41	35 38 40	syl2anc	⊢ ( 𝜑 → ( ( invg ‘ 𝑆 ) ‘ ( 1r ‘ 𝑆 ) ) ∈ ( Base ‘ 𝑆 ) )
42	2 17 6 16 7 8 10 33 41	lkrss	⊢ ( 𝜑 → ( 𝐿 ‘ ( ( ( 𝐼 ‘ ( 𝐺 ‘ 𝑋 ) ) × ( 𝐸 ‘ 𝑋 ) ) · 𝐺 ) ) ⊆ ( 𝐿 ‘ ( ( ( invg ‘ 𝑆 ) ‘ ( 1r ‘ 𝑆 ) ) · ( ( ( 𝐼 ‘ ( 𝐺 ‘ 𝑋 ) ) × ( 𝐸 ‘ 𝑋 ) ) · 𝐺 ) ) ) )
43	32 42	sstrd	⊢ ( 𝜑 → ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ ( ( ( invg ‘ 𝑆 ) ‘ ( 1r ‘ 𝑆 ) ) · ( ( ( 𝐼 ‘ ( 𝐺 ‘ 𝑋 ) ) × ( 𝐸 ‘ 𝑋 ) ) · 𝐺 ) ) ) )
44		sslin	⊢ ( ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ ( ( ( invg ‘ 𝑆 ) ‘ ( 1r ‘ 𝑆 ) ) · ( ( ( 𝐼 ‘ ( 𝐺 ‘ 𝑋 ) ) × ( 𝐸 ‘ 𝑋 ) ) · 𝐺 ) ) ) → ( ( 𝐿 ‘ 𝐸 ) ∩ ( 𝐿 ‘ 𝐺 ) ) ⊆ ( ( 𝐿 ‘ 𝐸 ) ∩ ( 𝐿 ‘ ( ( ( invg ‘ 𝑆 ) ‘ ( 1r ‘ 𝑆 ) ) · ( ( ( 𝐼 ‘ ( 𝐺 ‘ 𝑋 ) ) × ( 𝐸 ‘ 𝑋 ) ) · 𝐺 ) ) ) ) )
45	43 44	syl	⊢ ( 𝜑 → ( ( 𝐿 ‘ 𝐸 ) ∩ ( 𝐿 ‘ 𝐺 ) ) ⊆ ( ( 𝐿 ‘ 𝐸 ) ∩ ( 𝐿 ‘ ( ( ( invg ‘ 𝑆 ) ‘ ( 1r ‘ 𝑆 ) ) · ( ( ( 𝐼 ‘ ( 𝐺 ‘ 𝑋 ) ) × ( 𝐸 ‘ 𝑋 ) ) · 𝐺 ) ) ) ) )
46		eqid	⊢ ( +g ‘ 𝐷 ) = ( +g ‘ 𝐷 )
47	6 2 17 7 8 19 41 33	ldualvscl	⊢ ( 𝜑 → ( ( ( invg ‘ 𝑆 ) ‘ ( 1r ‘ 𝑆 ) ) · ( ( ( 𝐼 ‘ ( 𝐺 ‘ 𝑋 ) ) × ( 𝐸 ‘ 𝑋 ) ) · 𝐺 ) ) ∈ 𝐹 )
48	6 16 7 46 19 11 47	lkrin	⊢ ( 𝜑 → ( ( 𝐿 ‘ 𝐸 ) ∩ ( 𝐿 ‘ ( ( ( invg ‘ 𝑆 ) ‘ ( 1r ‘ 𝑆 ) ) · ( ( ( 𝐼 ‘ ( 𝐺 ‘ 𝑋 ) ) × ( 𝐸 ‘ 𝑋 ) ) · 𝐺 ) ) ) ) ⊆ ( 𝐿 ‘ ( 𝐸 ( +g ‘ 𝐷 ) ( ( ( invg ‘ 𝑆 ) ‘ ( 1r ‘ 𝑆 ) ) · ( ( ( 𝐼 ‘ ( 𝐺 ‘ 𝑋 ) ) × ( 𝐸 ‘ 𝑋 ) ) · 𝐺 ) ) ) ) )
49	45 48	sstrd	⊢ ( 𝜑 → ( ( 𝐿 ‘ 𝐸 ) ∩ ( 𝐿 ‘ 𝐺 ) ) ⊆ ( 𝐿 ‘ ( 𝐸 ( +g ‘ 𝐷 ) ( ( ( invg ‘ 𝑆 ) ‘ ( 1r ‘ 𝑆 ) ) · ( ( ( 𝐼 ‘ ( 𝐺 ‘ 𝑋 ) ) × ( 𝐸 ‘ 𝑋 ) ) · 𝐺 ) ) ) ) )
50	15	fveq2i	⊢ ( 𝐿 ‘ 𝐻 ) = ( 𝐿 ‘ ( 𝐸 − ( ( ( 𝐼 ‘ ( 𝐺 ‘ 𝑋 ) ) × ( 𝐸 ‘ 𝑋 ) ) · 𝐺 ) ) )
51	2 39 36 6 7 46 8 9 19 11 33	ldualvsub	⊢ ( 𝜑 → ( 𝐸 − ( ( ( 𝐼 ‘ ( 𝐺 ‘ 𝑋 ) ) × ( 𝐸 ‘ 𝑋 ) ) · 𝐺 ) ) = ( 𝐸 ( +g ‘ 𝐷 ) ( ( ( invg ‘ 𝑆 ) ‘ ( 1r ‘ 𝑆 ) ) · ( ( ( 𝐼 ‘ ( 𝐺 ‘ 𝑋 ) ) × ( 𝐸 ‘ 𝑋 ) ) · 𝐺 ) ) ) )
52	51	fveq2d	⊢ ( 𝜑 → ( 𝐿 ‘ ( 𝐸 − ( ( ( 𝐼 ‘ ( 𝐺 ‘ 𝑋 ) ) × ( 𝐸 ‘ 𝑋 ) ) · 𝐺 ) ) ) = ( 𝐿 ‘ ( 𝐸 ( +g ‘ 𝐷 ) ( ( ( invg ‘ 𝑆 ) ‘ ( 1r ‘ 𝑆 ) ) · ( ( ( 𝐼 ‘ ( 𝐺 ‘ 𝑋 ) ) × ( 𝐸 ‘ 𝑋 ) ) · 𝐺 ) ) ) ) )
53	50 52	eqtr2id	⊢ ( 𝜑 → ( 𝐿 ‘ ( 𝐸 ( +g ‘ 𝐷 ) ( ( ( invg ‘ 𝑆 ) ‘ ( 1r ‘ 𝑆 ) ) · ( ( ( 𝐼 ‘ ( 𝐺 ‘ 𝑋 ) ) × ( 𝐸 ‘ 𝑋 ) ) · 𝐺 ) ) ) ) = ( 𝐿 ‘ 𝐻 ) )
54	49 53	sseqtrd	⊢ ( 𝜑 → ( ( 𝐿 ‘ 𝐸 ) ∩ ( 𝐿 ‘ 𝐺 ) ) ⊆ ( 𝐿 ‘ 𝐻 ) )