Metamath Proof Explorer

Theorem lcfrlem1

Description: Lemma for lcfr . Note that X is z in Mario's notes. (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 ⊢ 𝐻 = ( 𝐸 − ( ( ( 𝐼 ‘ ( 𝐺 ‘ 𝑋 ) ) × ( 𝐸 ‘ 𝑋 ) ) · 𝐺 ) )
Assertion lcfrlem1 ( 𝜑 → ( 𝐻 ‘ 𝑋 ) = 0 )

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 15 fveq1i ⊢ ( 𝐻 ‘ 𝑋 ) = ( ( 𝐸 − ( ( ( 𝐼 ‘ ( 𝐺 ‘ 𝑋 ) ) × ( 𝐸 ‘ 𝑋 ) ) · 𝐺 ) ) ‘ 𝑋 )
17 eqid ⊢ ( -g ‘ 𝑆 ) = ( -g ‘ 𝑆 )
18 lveclmod ⊢ ( 𝑈 ∈ LVec → 𝑈 ∈ LMod )
19 10 18 syl ⊢ ( 𝜑 → 𝑈 ∈ LMod )
20 eqid ⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
21 2 lvecdrng ⊢ ( 𝑈 ∈ LVec → 𝑆 ∈ DivRing )
22 10 21 syl ⊢ ( 𝜑 → 𝑆 ∈ DivRing )
23 2 20 1 6 lflcl ⊢ ( ( 𝑈 ∈ LVec ∧ 𝐺 ∈ 𝐹 ∧ 𝑋 ∈ 𝑉 ) → ( 𝐺 ‘ 𝑋 ) ∈ ( Base ‘ 𝑆 ) )
24 10 12 13 23 syl3anc ⊢ ( 𝜑 → ( 𝐺 ‘ 𝑋 ) ∈ ( Base ‘ 𝑆 ) )
25 20 4 5 drnginvrcl ⊢ ( ( 𝑆 ∈ DivRing ∧ ( 𝐺 ‘ 𝑋 ) ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐺 ‘ 𝑋 ) ≠ 0 ) → ( 𝐼 ‘ ( 𝐺 ‘ 𝑋 ) ) ∈ ( Base ‘ 𝑆 ) )
26 22 24 14 25 syl3anc ⊢ ( 𝜑 → ( 𝐼 ‘ ( 𝐺 ‘ 𝑋 ) ) ∈ ( Base ‘ 𝑆 ) )
27 2 20 1 6 lflcl ⊢ ( ( 𝑈 ∈ LVec ∧ 𝐸 ∈ 𝐹 ∧ 𝑋 ∈ 𝑉 ) → ( 𝐸 ‘ 𝑋 ) ∈ ( Base ‘ 𝑆 ) )
28 10 11 13 27 syl3anc ⊢ ( 𝜑 → ( 𝐸 ‘ 𝑋 ) ∈ ( Base ‘ 𝑆 ) )
29 2 20 3 lmodmcl ⊢ ( ( 𝑈 ∈ LMod ∧ ( 𝐼 ‘ ( 𝐺 ‘ 𝑋 ) ) ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐸 ‘ 𝑋 ) ∈ ( Base ‘ 𝑆 ) ) → ( ( 𝐼 ‘ ( 𝐺 ‘ 𝑋 ) ) × ( 𝐸 ‘ 𝑋 ) ) ∈ ( Base ‘ 𝑆 ) )
30 19 26 28 29 syl3anc ⊢ ( 𝜑 → ( ( 𝐼 ‘ ( 𝐺 ‘ 𝑋 ) ) × ( 𝐸 ‘ 𝑋 ) ) ∈ ( Base ‘ 𝑆 ) )
31 6 2 20 7 8 19 30 12 ldualvscl ⊢ ( 𝜑 → ( ( ( 𝐼 ‘ ( 𝐺 ‘ 𝑋 ) ) × ( 𝐸 ‘ 𝑋 ) ) · 𝐺 ) ∈ 𝐹 )
32 1 2 17 6 7 9 19 11 31 13 ldualvsubval ⊢ ( 𝜑 → ( ( 𝐸 − ( ( ( 𝐼 ‘ ( 𝐺 ‘ 𝑋 ) ) × ( 𝐸 ‘ 𝑋 ) ) · 𝐺 ) ) ‘ 𝑋 ) = ( ( 𝐸 ‘ 𝑋 ) ( -g ‘ 𝑆 ) ( ( ( ( 𝐼 ‘ ( 𝐺 ‘ 𝑋 ) ) × ( 𝐸 ‘ 𝑋 ) ) · 𝐺 ) ‘ 𝑋 ) ) )
33 6 1 2 20 3 7 8 10 30 12 13 ldualvsval ⊢ ( 𝜑 → ( ( ( ( 𝐼 ‘ ( 𝐺 ‘ 𝑋 ) ) × ( 𝐸 ‘ 𝑋 ) ) · 𝐺 ) ‘ 𝑋 ) = ( ( 𝐺 ‘ 𝑋 ) × ( ( 𝐼 ‘ ( 𝐺 ‘ 𝑋 ) ) × ( 𝐸 ‘ 𝑋 ) ) ) )
34 eqid ⊢ ( 1r ‘ 𝑆 ) = ( 1r ‘ 𝑆 )
35 20 4 3 34 5 drnginvrr ⊢ ( ( 𝑆 ∈ DivRing ∧ ( 𝐺 ‘ 𝑋 ) ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐺 ‘ 𝑋 ) ≠ 0 ) → ( ( 𝐺 ‘ 𝑋 ) × ( 𝐼 ‘ ( 𝐺 ‘ 𝑋 ) ) ) = ( 1r ‘ 𝑆 ) )
36 22 24 14 35 syl3anc ⊢ ( 𝜑 → ( ( 𝐺 ‘ 𝑋 ) × ( 𝐼 ‘ ( 𝐺 ‘ 𝑋 ) ) ) = ( 1r ‘ 𝑆 ) )
37 36 oveq1d ⊢ ( 𝜑 → ( ( ( 𝐺 ‘ 𝑋 ) × ( 𝐼 ‘ ( 𝐺 ‘ 𝑋 ) ) ) × ( 𝐸 ‘ 𝑋 ) ) = ( ( 1r ‘ 𝑆 ) × ( 𝐸 ‘ 𝑋 ) ) )
38 2 lmodring ⊢ ( 𝑈 ∈ LMod → 𝑆 ∈ Ring )
39 19 38 syl ⊢ ( 𝜑 → 𝑆 ∈ Ring )
40 20 3 ringass ⊢ ( ( 𝑆 ∈ Ring ∧ ( ( 𝐺 ‘ 𝑋 ) ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐼 ‘ ( 𝐺 ‘ 𝑋 ) ) ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐸 ‘ 𝑋 ) ∈ ( Base ‘ 𝑆 ) ) ) → ( ( ( 𝐺 ‘ 𝑋 ) × ( 𝐼 ‘ ( 𝐺 ‘ 𝑋 ) ) ) × ( 𝐸 ‘ 𝑋 ) ) = ( ( 𝐺 ‘ 𝑋 ) × ( ( 𝐼 ‘ ( 𝐺 ‘ 𝑋 ) ) × ( 𝐸 ‘ 𝑋 ) ) ) )
41 39 24 26 28 40 syl13anc ⊢ ( 𝜑 → ( ( ( 𝐺 ‘ 𝑋 ) × ( 𝐼 ‘ ( 𝐺 ‘ 𝑋 ) ) ) × ( 𝐸 ‘ 𝑋 ) ) = ( ( 𝐺 ‘ 𝑋 ) × ( ( 𝐼 ‘ ( 𝐺 ‘ 𝑋 ) ) × ( 𝐸 ‘ 𝑋 ) ) ) )
42 20 3 34 ringlidm ⊢ ( ( 𝑆 ∈ Ring ∧ ( 𝐸 ‘ 𝑋 ) ∈ ( Base ‘ 𝑆 ) ) → ( ( 1r ‘ 𝑆 ) × ( 𝐸 ‘ 𝑋 ) ) = ( 𝐸 ‘ 𝑋 ) )
43 39 28 42 syl2anc ⊢ ( 𝜑 → ( ( 1r ‘ 𝑆 ) × ( 𝐸 ‘ 𝑋 ) ) = ( 𝐸 ‘ 𝑋 ) )
44 37 41 43 3eqtr3d ⊢ ( 𝜑 → ( ( 𝐺 ‘ 𝑋 ) × ( ( 𝐼 ‘ ( 𝐺 ‘ 𝑋 ) ) × ( 𝐸 ‘ 𝑋 ) ) ) = ( 𝐸 ‘ 𝑋 ) )
45 33 44 eqtrd ⊢ ( 𝜑 → ( ( ( ( 𝐼 ‘ ( 𝐺 ‘ 𝑋 ) ) × ( 𝐸 ‘ 𝑋 ) ) · 𝐺 ) ‘ 𝑋 ) = ( 𝐸 ‘ 𝑋 ) )
46 45 oveq2d ⊢ ( 𝜑 → ( ( 𝐸 ‘ 𝑋 ) ( -g ‘ 𝑆 ) ( ( ( ( 𝐼 ‘ ( 𝐺 ‘ 𝑋 ) ) × ( 𝐸 ‘ 𝑋 ) ) · 𝐺 ) ‘ 𝑋 ) ) = ( ( 𝐸 ‘ 𝑋 ) ( -g ‘ 𝑆 ) ( 𝐸 ‘ 𝑋 ) ) )
47 2 lmodfgrp ⊢ ( 𝑈 ∈ LMod → 𝑆 ∈ Grp )
48 19 47 syl ⊢ ( 𝜑 → 𝑆 ∈ Grp )
49 20 4 17 grpsubid ⊢ ( ( 𝑆 ∈ Grp ∧ ( 𝐸 ‘ 𝑋 ) ∈ ( Base ‘ 𝑆 ) ) → ( ( 𝐸 ‘ 𝑋 ) ( -g ‘ 𝑆 ) ( 𝐸 ‘ 𝑋 ) ) = 0 )
50 48 28 49 syl2anc ⊢ ( 𝜑 → ( ( 𝐸 ‘ 𝑋 ) ( -g ‘ 𝑆 ) ( 𝐸 ‘ 𝑋 ) ) = 0 )
51 32 46 50 3eqtrd ⊢ ( 𝜑 → ( ( 𝐸 − ( ( ( 𝐼 ‘ ( 𝐺 ‘ 𝑋 ) ) × ( 𝐸 ‘ 𝑋 ) ) · 𝐺 ) ) ‘ 𝑋 ) = 0 )
52 16 51 syl5eq ⊢ ( 𝜑 → ( 𝐻 ‘ 𝑋 ) = 0 )