Metamath Proof Explorer


Theorem lincresunitlem2

Description: Lemma for properties of a specially modified restriction of a linear combination containing a unit as scalar. (Contributed by AV, 18-May-2019)

Ref Expression
Hypotheses lincresunit.b B = Base M
lincresunit.r R = Scalar M
lincresunit.e E = Base R
lincresunit.u U = Unit R
lincresunit.0 0 ˙ = 0 R
lincresunit.z Z = 0 M
lincresunit.n N = inv g R
lincresunit.i I = inv r R
lincresunit.t · ˙ = R
lincresunit.g G = s S X I N F X · ˙ F s
Assertion lincresunitlem2 S 𝒫 B M LMod X S F E S F X U Y S I N F X · ˙ F Y E

Proof

Step Hyp Ref Expression
1 lincresunit.b B = Base M
2 lincresunit.r R = Scalar M
3 lincresunit.e E = Base R
4 lincresunit.u U = Unit R
5 lincresunit.0 0 ˙ = 0 R
6 lincresunit.z Z = 0 M
7 lincresunit.n N = inv g R
8 lincresunit.i I = inv r R
9 lincresunit.t · ˙ = R
10 lincresunit.g G = s S X I N F X · ˙ F s
11 2 lmodring M LMod R Ring
12 11 3ad2ant2 S 𝒫 B M LMod X S R Ring
13 12 adantr S 𝒫 B M LMod X S F E S F X U R Ring
14 13 adantr S 𝒫 B M LMod X S F E S F X U Y S R Ring
15 1 2 3 4 5 6 7 8 9 10 lincresunitlem1 S 𝒫 B M LMod X S F E S F X U I N F X E
16 15 adantr S 𝒫 B M LMod X S F E S F X U Y S I N F X E
17 elmapi F E S F : S E
18 ffvelrn F : S E Y S F Y E
19 18 ex F : S E Y S F Y E
20 17 19 syl F E S Y S F Y E
21 20 ad2antrl S 𝒫 B M LMod X S F E S F X U Y S F Y E
22 21 imp S 𝒫 B M LMod X S F E S F X U Y S F Y E
23 3 9 ringcl R Ring I N F X E F Y E I N F X · ˙ F Y E
24 14 16 22 23 syl3anc S 𝒫 B M LMod X S F E S F X U Y S I N F X · ˙ F Y E