Metamath Proof Explorer


Theorem lincresunit1

Description: Property 1 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 lincresunit1 ( ( ( 𝑆 ∈ 𝒫 𝐵𝑀 ∈ LMod ∧ 𝑋𝑆 ) ∧ ( 𝐹 ∈ ( 𝐸m 𝑆 ) ∧ ( 𝐹𝑋 ) ∈ 𝑈 ) ) → 𝐺 ∈ ( 𝐸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 eldifi ( 𝑠 ∈ ( 𝑆 ∖ { 𝑋 } ) → 𝑠𝑆 )
12 1 2 3 4 5 6 7 8 9 10 lincresunitlem2 ( ( ( ( 𝑆 ∈ 𝒫 𝐵𝑀 ∈ LMod ∧ 𝑋𝑆 ) ∧ ( 𝐹 ∈ ( 𝐸m 𝑆 ) ∧ ( 𝐹𝑋 ) ∈ 𝑈 ) ) ∧ 𝑠𝑆 ) → ( ( 𝐼 ‘ ( 𝑁 ‘ ( 𝐹𝑋 ) ) ) · ( 𝐹𝑠 ) ) ∈ 𝐸 )
13 11 12 sylan2 ( ( ( ( 𝑆 ∈ 𝒫 𝐵𝑀 ∈ LMod ∧ 𝑋𝑆 ) ∧ ( 𝐹 ∈ ( 𝐸m 𝑆 ) ∧ ( 𝐹𝑋 ) ∈ 𝑈 ) ) ∧ 𝑠 ∈ ( 𝑆 ∖ { 𝑋 } ) ) → ( ( 𝐼 ‘ ( 𝑁 ‘ ( 𝐹𝑋 ) ) ) · ( 𝐹𝑠 ) ) ∈ 𝐸 )
14 13 fmpttd ( ( ( 𝑆 ∈ 𝒫 𝐵𝑀 ∈ LMod ∧ 𝑋𝑆 ) ∧ ( 𝐹 ∈ ( 𝐸m 𝑆 ) ∧ ( 𝐹𝑋 ) ∈ 𝑈 ) ) → ( 𝑠 ∈ ( 𝑆 ∖ { 𝑋 } ) ↦ ( ( 𝐼 ‘ ( 𝑁 ‘ ( 𝐹𝑋 ) ) ) · ( 𝐹𝑠 ) ) ) : ( 𝑆 ∖ { 𝑋 } ) ⟶ 𝐸 )
15 3 fvexi 𝐸 ∈ V
16 difexg ( 𝑆 ∈ 𝒫 𝐵 → ( 𝑆 ∖ { 𝑋 } ) ∈ V )
17 16 3ad2ant1 ( ( 𝑆 ∈ 𝒫 𝐵𝑀 ∈ LMod ∧ 𝑋𝑆 ) → ( 𝑆 ∖ { 𝑋 } ) ∈ V )
18 17 adantr ( ( ( 𝑆 ∈ 𝒫 𝐵𝑀 ∈ LMod ∧ 𝑋𝑆 ) ∧ ( 𝐹 ∈ ( 𝐸m 𝑆 ) ∧ ( 𝐹𝑋 ) ∈ 𝑈 ) ) → ( 𝑆 ∖ { 𝑋 } ) ∈ V )
19 elmapg ( ( 𝐸 ∈ V ∧ ( 𝑆 ∖ { 𝑋 } ) ∈ V ) → ( ( 𝑠 ∈ ( 𝑆 ∖ { 𝑋 } ) ↦ ( ( 𝐼 ‘ ( 𝑁 ‘ ( 𝐹𝑋 ) ) ) · ( 𝐹𝑠 ) ) ) ∈ ( 𝐸m ( 𝑆 ∖ { 𝑋 } ) ) ↔ ( 𝑠 ∈ ( 𝑆 ∖ { 𝑋 } ) ↦ ( ( 𝐼 ‘ ( 𝑁 ‘ ( 𝐹𝑋 ) ) ) · ( 𝐹𝑠 ) ) ) : ( 𝑆 ∖ { 𝑋 } ) ⟶ 𝐸 ) )
20 15 18 19 sylancr ( ( ( 𝑆 ∈ 𝒫 𝐵𝑀 ∈ LMod ∧ 𝑋𝑆 ) ∧ ( 𝐹 ∈ ( 𝐸m 𝑆 ) ∧ ( 𝐹𝑋 ) ∈ 𝑈 ) ) → ( ( 𝑠 ∈ ( 𝑆 ∖ { 𝑋 } ) ↦ ( ( 𝐼 ‘ ( 𝑁 ‘ ( 𝐹𝑋 ) ) ) · ( 𝐹𝑠 ) ) ) ∈ ( 𝐸m ( 𝑆 ∖ { 𝑋 } ) ) ↔ ( 𝑠 ∈ ( 𝑆 ∖ { 𝑋 } ) ↦ ( ( 𝐼 ‘ ( 𝑁 ‘ ( 𝐹𝑋 ) ) ) · ( 𝐹𝑠 ) ) ) : ( 𝑆 ∖ { 𝑋 } ) ⟶ 𝐸 ) )
21 14 20 mpbird ( ( ( 𝑆 ∈ 𝒫 𝐵𝑀 ∈ LMod ∧ 𝑋𝑆 ) ∧ ( 𝐹 ∈ ( 𝐸m 𝑆 ) ∧ ( 𝐹𝑋 ) ∈ 𝑈 ) ) → ( 𝑠 ∈ ( 𝑆 ∖ { 𝑋 } ) ↦ ( ( 𝐼 ‘ ( 𝑁 ‘ ( 𝐹𝑋 ) ) ) · ( 𝐹𝑠 ) ) ) ∈ ( 𝐸m ( 𝑆 ∖ { 𝑋 } ) ) )
22 10 21 eqeltrid ( ( ( 𝑆 ∈ 𝒫 𝐵𝑀 ∈ LMod ∧ 𝑋𝑆 ) ∧ ( 𝐹 ∈ ( 𝐸m 𝑆 ) ∧ ( 𝐹𝑋 ) ∈ 𝑈 ) ) → 𝐺 ∈ ( 𝐸m ( 𝑆 ∖ { 𝑋 } ) ) )