Metamath Proof Explorer

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 ⊢ ( 𝜑 → ( ( 𝐿 ‘ 𝐸 ) ∩ ( 𝐿 ‘ 𝐺 ) ) ⊆ ( 𝐿 ‘ 𝐻 ) )