Metamath Proof Explorer

Theorem lclkrlem2m

Description: Lemma for lclkr . Construct a vector B that makes the sum of functionals zero. Combine with B e. V to shorten overall proof. (Contributed by NM, 17-Jan-2015)

Ref Expression
Hypotheses lclkrlem2m.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
lclkrlem2m.t ⊢ · = ( ·𝑠 ‘ 𝑈 )
lclkrlem2m.s ⊢ 𝑆 = ( Scalar ‘ 𝑈 )
lclkrlem2m.q ⊢ × = ( .r ‘ 𝑆 )
lclkrlem2m.z ⊢ 0 = ( 0g ‘ 𝑆 )
lclkrlem2m.i ⊢ 𝐼 = ( invr ‘ 𝑆 )
lclkrlem2m.m ⊢ − = ( -g ‘ 𝑈 )
lclkrlem2m.f ⊢ 𝐹 = ( LFnl ‘ 𝑈 )
lclkrlem2m.d ⊢ 𝐷 = ( LDual ‘ 𝑈 )
lclkrlem2m.p ⊢ + = ( +g ‘ 𝐷 )
lclkrlem2m.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
lclkrlem2m.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
lclkrlem2m.e ⊢ ( 𝜑 → 𝐸 ∈ 𝐹 )
lclkrlem2m.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
lclkrlem2m.w ⊢ ( 𝜑 → 𝑈 ∈ LVec )
lclkrlem2m.b ⊢ 𝐵 = ( 𝑋 − ( ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) × ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ) · 𝑌 ) )
lclkrlem2m.n ⊢ ( 𝜑 → ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ≠ 0 )
Assertion lclkrlem2m ( 𝜑 → ( 𝐵 ∈ 𝑉 ∧ ( ( 𝐸 + 𝐺 ) ‘ 𝐵 ) = 0 ) )

Proof

Step Hyp Ref Expression
1 lclkrlem2m.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
2 lclkrlem2m.t ⊢ · = ( ·𝑠 ‘ 𝑈 )
3 lclkrlem2m.s ⊢ 𝑆 = ( Scalar ‘ 𝑈 )
4 lclkrlem2m.q ⊢ × = ( .r ‘ 𝑆 )
5 lclkrlem2m.z ⊢ 0 = ( 0g ‘ 𝑆 )
6 lclkrlem2m.i ⊢ 𝐼 = ( invr ‘ 𝑆 )
7 lclkrlem2m.m ⊢ − = ( -g ‘ 𝑈 )
8 lclkrlem2m.f ⊢ 𝐹 = ( LFnl ‘ 𝑈 )
9 lclkrlem2m.d ⊢ 𝐷 = ( LDual ‘ 𝑈 )
10 lclkrlem2m.p ⊢ + = ( +g ‘ 𝐷 )
11 lclkrlem2m.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
12 lclkrlem2m.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
13 lclkrlem2m.e ⊢ ( 𝜑 → 𝐸 ∈ 𝐹 )
14 lclkrlem2m.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
15 lclkrlem2m.w ⊢ ( 𝜑 → 𝑈 ∈ LVec )
16 lclkrlem2m.b ⊢ 𝐵 = ( 𝑋 − ( ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) × ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ) · 𝑌 ) )
17 lclkrlem2m.n ⊢ ( 𝜑 → ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ≠ 0 )
18 lveclmod ⊢ ( 𝑈 ∈ LVec → 𝑈 ∈ LMod )
19 15 18 syl ⊢ ( 𝜑 → 𝑈 ∈ LMod )
20 lmodgrp ⊢ ( 𝑈 ∈ LMod → 𝑈 ∈ Grp )
21 19 20 syl ⊢ ( 𝜑 → 𝑈 ∈ Grp )
22 3 lmodring ⊢ ( 𝑈 ∈ LMod → 𝑆 ∈ Ring )
23 19 22 syl ⊢ ( 𝜑 → 𝑆 ∈ Ring )
24 8 9 10 19 13 14 ldualvaddcl ⊢ ( 𝜑 → ( 𝐸 + 𝐺 ) ∈ 𝐹 )
25 eqid ⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
26 3 25 1 8 lflcl ⊢ ( ( 𝑈 ∈ LVec ∧ ( 𝐸 + 𝐺 ) ∈ 𝐹 ∧ 𝑋 ∈ 𝑉 ) → ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) ∈ ( Base ‘ 𝑆 ) )
27 15 24 11 26 syl3anc ⊢ ( 𝜑 → ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) ∈ ( Base ‘ 𝑆 ) )
28 3 lvecdrng ⊢ ( 𝑈 ∈ LVec → 𝑆 ∈ DivRing )
29 15 28 syl ⊢ ( 𝜑 → 𝑆 ∈ DivRing )
30 3 25 1 8 lflcl ⊢ ( ( 𝑈 ∈ LVec ∧ ( 𝐸 + 𝐺 ) ∈ 𝐹 ∧ 𝑌 ∈ 𝑉 ) → ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ∈ ( Base ‘ 𝑆 ) )
31 15 24 12 30 syl3anc ⊢ ( 𝜑 → ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ∈ ( Base ‘ 𝑆 ) )
32 25 5 6 drnginvrcl ⊢ ( ( 𝑆 ∈ DivRing ∧ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ∈ ( Base ‘ 𝑆 ) ∧ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ≠ 0 ) → ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ∈ ( Base ‘ 𝑆 ) )
33 29 31 17 32 syl3anc ⊢ ( 𝜑 → ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ∈ ( Base ‘ 𝑆 ) )
34 25 4 ringcl ⊢ ( ( 𝑆 ∈ Ring ∧ ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ∈ ( Base ‘ 𝑆 ) ) → ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) × ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ) ∈ ( Base ‘ 𝑆 ) )
35 23 27 33 34 syl3anc ⊢ ( 𝜑 → ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) × ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ) ∈ ( Base ‘ 𝑆 ) )
36 1 3 2 25 lmodvscl ⊢ ( ( 𝑈 ∈ LMod ∧ ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) × ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ) ∈ ( Base ‘ 𝑆 ) ∧ 𝑌 ∈ 𝑉 ) → ( ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) × ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ) · 𝑌 ) ∈ 𝑉 )
37 19 35 12 36 syl3anc ⊢ ( 𝜑 → ( ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) × ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ) · 𝑌 ) ∈ 𝑉 )
38 1 7 grpsubcl ⊢ ( ( 𝑈 ∈ Grp ∧ 𝑋 ∈ 𝑉 ∧ ( ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) × ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ) · 𝑌 ) ∈ 𝑉 ) → ( 𝑋 − ( ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) × ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ) · 𝑌 ) ) ∈ 𝑉 )
39 21 11 37 38 syl3anc ⊢ ( 𝜑 → ( 𝑋 − ( ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) × ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ) · 𝑌 ) ) ∈ 𝑉 )
40 16 39 eqeltrid ⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
41 16 fveq2i ⊢ ( ( 𝐸 + 𝐺 ) ‘ 𝐵 ) = ( ( 𝐸 + 𝐺 ) ‘ ( 𝑋 − ( ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) × ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ) · 𝑌 ) ) )
42 eqid ⊢ ( -g ‘ 𝑆 ) = ( -g ‘ 𝑆 )
43 3 42 1 7 8 lflsub ⊢ ( ( 𝑈 ∈ LMod ∧ ( 𝐸 + 𝐺 ) ∈ 𝐹 ∧ ( 𝑋 ∈ 𝑉 ∧ ( ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) × ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ) · 𝑌 ) ∈ 𝑉 ) ) → ( ( 𝐸 + 𝐺 ) ‘ ( 𝑋 − ( ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) × ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ) · 𝑌 ) ) ) = ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) ( -g ‘ 𝑆 ) ( ( 𝐸 + 𝐺 ) ‘ ( ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) × ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ) · 𝑌 ) ) ) )
44 19 24 11 37 43 syl112anc ⊢ ( 𝜑 → ( ( 𝐸 + 𝐺 ) ‘ ( 𝑋 − ( ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) × ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ) · 𝑌 ) ) ) = ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) ( -g ‘ 𝑆 ) ( ( 𝐸 + 𝐺 ) ‘ ( ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) × ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ) · 𝑌 ) ) ) )
45 3 25 4 1 2 8 lflmul ⊢ ( ( 𝑈 ∈ LMod ∧ ( 𝐸 + 𝐺 ) ∈ 𝐹 ∧ ( ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) × ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ) ∈ ( Base ‘ 𝑆 ) ∧ 𝑌 ∈ 𝑉 ) ) → ( ( 𝐸 + 𝐺 ) ‘ ( ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) × ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ) · 𝑌 ) ) = ( ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) × ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ) × ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) )
46 19 24 35 12 45 syl112anc ⊢ ( 𝜑 → ( ( 𝐸 + 𝐺 ) ‘ ( ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) × ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ) · 𝑌 ) ) = ( ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) × ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ) × ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) )
47 25 4 ringass ⊢ ( ( 𝑆 ∈ Ring ∧ ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ∈ ( Base ‘ 𝑆 ) ∧ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ∈ ( Base ‘ 𝑆 ) ) ) → ( ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) × ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ) × ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) = ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) × ( ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) × ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ) )
48 23 27 33 31 47 syl13anc ⊢ ( 𝜑 → ( ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) × ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ) × ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) = ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) × ( ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) × ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ) )
49 eqid ⊢ ( 1r ‘ 𝑆 ) = ( 1r ‘ 𝑆 )
50 25 5 4 49 6 drnginvrl ⊢ ( ( 𝑆 ∈ DivRing ∧ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ∈ ( Base ‘ 𝑆 ) ∧ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ≠ 0 ) → ( ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) × ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) = ( 1r ‘ 𝑆 ) )
51 29 31 17 50 syl3anc ⊢ ( 𝜑 → ( ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) × ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) = ( 1r ‘ 𝑆 ) )
52 51 oveq2d ⊢ ( 𝜑 → ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) × ( ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) × ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ) = ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) × ( 1r ‘ 𝑆 ) ) )
53 48 52 eqtrd ⊢ ( 𝜑 → ( ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) × ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ) × ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) = ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) × ( 1r ‘ 𝑆 ) ) )
54 25 4 49 ringridm ⊢ ( ( 𝑆 ∈ Ring ∧ ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) ∈ ( Base ‘ 𝑆 ) ) → ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) × ( 1r ‘ 𝑆 ) ) = ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) )
55 23 27 54 syl2anc ⊢ ( 𝜑 → ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) × ( 1r ‘ 𝑆 ) ) = ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) )
56 46 53 55 3eqtrd ⊢ ( 𝜑 → ( ( 𝐸 + 𝐺 ) ‘ ( ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) × ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ) · 𝑌 ) ) = ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) )
57 56 oveq2d ⊢ ( 𝜑 → ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) ( -g ‘ 𝑆 ) ( ( 𝐸 + 𝐺 ) ‘ ( ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) × ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ) · 𝑌 ) ) ) = ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) ( -g ‘ 𝑆 ) ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) ) )
58 ringgrp ⊢ ( 𝑆 ∈ Ring → 𝑆 ∈ Grp )
59 23 58 syl ⊢ ( 𝜑 → 𝑆 ∈ Grp )
60 25 5 42 grpsubid ⊢ ( ( 𝑆 ∈ Grp ∧ ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) ∈ ( Base ‘ 𝑆 ) ) → ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) ( -g ‘ 𝑆 ) ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) ) = 0 )
61 59 27 60 syl2anc ⊢ ( 𝜑 → ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) ( -g ‘ 𝑆 ) ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) ) = 0 )
62 44 57 61 3eqtrd ⊢ ( 𝜑 → ( ( 𝐸 + 𝐺 ) ‘ ( 𝑋 − ( ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) × ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ) · 𝑌 ) ) ) = 0 )
63 41 62 syl5eq ⊢ ( 𝜑 → ( ( 𝐸 + 𝐺 ) ‘ 𝐵 ) = 0 )
64 40 63 jca ⊢ ( 𝜑 → ( 𝐵 ∈ 𝑉 ∧ ( ( 𝐸 + 𝐺 ) ‘ 𝐵 ) = 0 ) )