Metamath Proof Explorer


Theorem lincresunitlem1

Description: Lemma 1 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 𝐵 = ( Base ‘ 𝑀 )
lincresunit.r 𝑅 = ( Scalar ‘ 𝑀 )
lincresunit.e 𝐸 = ( Base ‘ 𝑅 )
lincresunit.u 𝑈 = ( Unit ‘ 𝑅 )
lincresunit.0 0 = ( 0g𝑅 )
lincresunit.z 𝑍 = ( 0g𝑀 )
lincresunit.n 𝑁 = ( invg𝑅 )
lincresunit.i 𝐼 = ( invr𝑅 )
lincresunit.t · = ( .r𝑅 )
lincresunit.g 𝐺 = ( 𝑠 ∈ ( 𝑆 ∖ { 𝑋 } ) ↦ ( ( 𝐼 ‘ ( 𝑁 ‘ ( 𝐹𝑋 ) ) ) · ( 𝐹𝑠 ) ) )
Assertion lincresunitlem1 ( ( ( 𝑆 ∈ 𝒫 𝐵𝑀 ∈ LMod ∧ 𝑋𝑆 ) ∧ ( 𝐹 ∈ ( 𝐸m 𝑆 ) ∧ ( 𝐹𝑋 ) ∈ 𝑈 ) ) → ( 𝐼 ‘ ( 𝑁 ‘ ( 𝐹𝑋 ) ) ) ∈ 𝐸 )

Proof

Step Hyp Ref Expression
1 lincresunit.b 𝐵 = ( Base ‘ 𝑀 )
2 lincresunit.r 𝑅 = ( Scalar ‘ 𝑀 )
3 lincresunit.e 𝐸 = ( Base ‘ 𝑅 )
4 lincresunit.u 𝑈 = ( Unit ‘ 𝑅 )
5 lincresunit.0 0 = ( 0g𝑅 )
6 lincresunit.z 𝑍 = ( 0g𝑀 )
7 lincresunit.n 𝑁 = ( invg𝑅 )
8 lincresunit.i 𝐼 = ( invr𝑅 )
9 lincresunit.t · = ( .r𝑅 )
10 lincresunit.g 𝐺 = ( 𝑠 ∈ ( 𝑆 ∖ { 𝑋 } ) ↦ ( ( 𝐼 ‘ ( 𝑁 ‘ ( 𝐹𝑋 ) ) ) · ( 𝐹𝑠 ) ) )
11 2 lmodring ( 𝑀 ∈ LMod → 𝑅 ∈ Ring )
12 11 3ad2ant2 ( ( 𝑆 ∈ 𝒫 𝐵𝑀 ∈ LMod ∧ 𝑋𝑆 ) → 𝑅 ∈ Ring )
13 12 adantr ( ( ( 𝑆 ∈ 𝒫 𝐵𝑀 ∈ LMod ∧ 𝑋𝑆 ) ∧ ( 𝐹 ∈ ( 𝐸m 𝑆 ) ∧ ( 𝐹𝑋 ) ∈ 𝑈 ) ) → 𝑅 ∈ Ring )
14 simpr ( ( 𝐹 ∈ ( 𝐸m 𝑆 ) ∧ ( 𝐹𝑋 ) ∈ 𝑈 ) → ( 𝐹𝑋 ) ∈ 𝑈 )
15 4 7 unitnegcl ( ( 𝑅 ∈ Ring ∧ ( 𝐹𝑋 ) ∈ 𝑈 ) → ( 𝑁 ‘ ( 𝐹𝑋 ) ) ∈ 𝑈 )
16 12 14 15 syl2an ( ( ( 𝑆 ∈ 𝒫 𝐵𝑀 ∈ LMod ∧ 𝑋𝑆 ) ∧ ( 𝐹 ∈ ( 𝐸m 𝑆 ) ∧ ( 𝐹𝑋 ) ∈ 𝑈 ) ) → ( 𝑁 ‘ ( 𝐹𝑋 ) ) ∈ 𝑈 )
17 4 8 3 ringinvcl ( ( 𝑅 ∈ Ring ∧ ( 𝑁 ‘ ( 𝐹𝑋 ) ) ∈ 𝑈 ) → ( 𝐼 ‘ ( 𝑁 ‘ ( 𝐹𝑋 ) ) ) ∈ 𝐸 )
18 13 16 17 syl2anc ( ( ( 𝑆 ∈ 𝒫 𝐵𝑀 ∈ LMod ∧ 𝑋𝑆 ) ∧ ( 𝐹 ∈ ( 𝐸m 𝑆 ) ∧ ( 𝐹𝑋 ) ∈ 𝑈 ) ) → ( 𝐼 ‘ ( 𝑁 ‘ ( 𝐹𝑋 ) ) ) ∈ 𝐸 )