Theorem lcfrlem3

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	lcfrlem3	⊢ ( 𝜑 → 𝑋 ∈ ( 𝐿 ‘ 𝐻 ) )

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	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15	lcfrlem1	⊢ ( 𝜑 → ( 𝐻 ‘ 𝑋 ) = 0 )
18		lveclmod	⊢ ( 𝑈 ∈ LVec → 𝑈 ∈ LMod )
19	10 18	syl	⊢ ( 𝜑 → 𝑈 ∈ LMod )
20		eqid	⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
21	2	lmodring	⊢ ( 𝑈 ∈ LMod → 𝑆 ∈ Ring )
22	19 21	syl	⊢ ( 𝜑 → 𝑆 ∈ Ring )
23	2	lvecdrng	⊢ ( 𝑈 ∈ LVec → 𝑆 ∈ DivRing )
24	10 23	syl	⊢ ( 𝜑 → 𝑆 ∈ DivRing )
25	2 20 1 6	lflcl	⊢ ( ( 𝑈 ∈ LVec ∧ 𝐺 ∈ 𝐹 ∧ 𝑋 ∈ 𝑉 ) → ( 𝐺 ‘ 𝑋 ) ∈ ( Base ‘ 𝑆 ) )
26	10 12 13 25	syl3anc	⊢ ( 𝜑 → ( 𝐺 ‘ 𝑋 ) ∈ ( Base ‘ 𝑆 ) )
27	20 4 5	drnginvrcl	⊢ ( ( 𝑆 ∈ DivRing ∧ ( 𝐺 ‘ 𝑋 ) ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐺 ‘ 𝑋 ) ≠ 0 ) → ( 𝐼 ‘ ( 𝐺 ‘ 𝑋 ) ) ∈ ( Base ‘ 𝑆 ) )
28	24 26 14 27	syl3anc	⊢ ( 𝜑 → ( 𝐼 ‘ ( 𝐺 ‘ 𝑋 ) ) ∈ ( Base ‘ 𝑆 ) )
29	2 20 1 6	lflcl	⊢ ( ( 𝑈 ∈ LVec ∧ 𝐸 ∈ 𝐹 ∧ 𝑋 ∈ 𝑉 ) → ( 𝐸 ‘ 𝑋 ) ∈ ( Base ‘ 𝑆 ) )
30	10 11 13 29	syl3anc	⊢ ( 𝜑 → ( 𝐸 ‘ 𝑋 ) ∈ ( Base ‘ 𝑆 ) )
31	20 3	ringcl	⊢ ( ( 𝑆 ∈ Ring ∧ ( 𝐼 ‘ ( 𝐺 ‘ 𝑋 ) ) ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐸 ‘ 𝑋 ) ∈ ( Base ‘ 𝑆 ) ) → ( ( 𝐼 ‘ ( 𝐺 ‘ 𝑋 ) ) × ( 𝐸 ‘ 𝑋 ) ) ∈ ( Base ‘ 𝑆 ) )
32	22 28 30 31	syl3anc	⊢ ( 𝜑 → ( ( 𝐼 ‘ ( 𝐺 ‘ 𝑋 ) ) × ( 𝐸 ‘ 𝑋 ) ) ∈ ( Base ‘ 𝑆 ) )
33	6 2 20 7 8 19 32 12	ldualvscl	⊢ ( 𝜑 → ( ( ( 𝐼 ‘ ( 𝐺 ‘ 𝑋 ) ) × ( 𝐸 ‘ 𝑋 ) ) · 𝐺 ) ∈ 𝐹 )
34	6 7 9 19 11 33	ldualvsubcl	⊢ ( 𝜑 → ( 𝐸 − ( ( ( 𝐼 ‘ ( 𝐺 ‘ 𝑋 ) ) × ( 𝐸 ‘ 𝑋 ) ) · 𝐺 ) ) ∈ 𝐹 )
35	15 34	eqeltrid	⊢ ( 𝜑 → 𝐻 ∈ 𝐹 )
36	1 2 4 6 16 10 35 13	ellkr2	⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝐿 ‘ 𝐻 ) ↔ ( 𝐻 ‘ 𝑋 ) = 0 ) )
37	17 36	mpbird	⊢ ( 𝜑 → 𝑋 ∈ ( 𝐿 ‘ 𝐻 ) )