# 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 $⊢ B = Base M$
lincresunit.r $⊢ R = Scalar ⁡ M$
lincresunit.e $⊢ E = Base R$
lincresunit.u $⊢ U = Unit ⁡ R$
lincresunit.0
lincresunit.z $⊢ Z = 0 M$
lincresunit.n $⊢ N = inv g ⁡ R$
lincresunit.i $⊢ I = inv r ⁡ R$
lincresunit.t
lincresunit.g
Assertion lincresunit1 $⊢ S ∈ 𝒫 B ∧ M ∈ LMod ∧ X ∈ S ∧ F ∈ E S ∧ F ⁡ X ∈ U → G ∈ E S ∖ X$

### 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
6 lincresunit.z $⊢ Z = 0 M$
7 lincresunit.n $⊢ N = inv g ⁡ R$
8 lincresunit.i $⊢ I = inv r ⁡ R$
9 lincresunit.t
10 lincresunit.g
11 eldifi $⊢ s ∈ S ∖ X → s ∈ S$
12 1 2 3 4 5 6 7 8 9 10 lincresunitlem2
13 11 12 sylan2
14 13 fmpttd
15 3 fvexi $⊢ E ∈ V$
16 difexg $⊢ S ∈ 𝒫 B → S ∖ X ∈ V$
17 16 3ad2ant1 $⊢ S ∈ 𝒫 B ∧ M ∈ LMod ∧ X ∈ S → S ∖ X ∈ V$
18 17 adantr $⊢ S ∈ 𝒫 B ∧ M ∈ LMod ∧ X ∈ S ∧ F ∈ E S ∧ F ⁡ X ∈ U → S ∖ X ∈ V$
19 elmapg
20 15 18 19 sylancr
21 14 20 mpbird
22 10 21 eqeltrid $⊢ S ∈ 𝒫 B ∧ M ∈ LMod ∧ X ∈ S ∧ F ∈ E S ∧ F ⁡ X ∈ U → G ∈ E S ∖ X$