# Metamath Proof Explorer

## Theorem frlmssuvc1

Description: A scalar multiple of a unit vector included in a support-restriction subspace is included in the subspace. (Contributed by Stefan O'Rear, 5-Feb-2015) (Revised by AV, 24-Jun-2019)

Ref Expression
Hypotheses frlmssuvc1.f 𝐹 = ( 𝑅 freeLMod 𝐼 )
frlmssuvc1.u 𝑈 = ( 𝑅 unitVec 𝐼 )
frlmssuvc1.b 𝐵 = ( Base ‘ 𝐹 )
frlmssuvc1.k 𝐾 = ( Base ‘ 𝑅 )
frlmssuvc1.t · = ( ·𝑠𝐹 )
frlmssuvc1.z 0 = ( 0g𝑅 )
frlmssuvc1.c 𝐶 = { 𝑥𝐵 ∣ ( 𝑥 supp 0 ) ⊆ 𝐽 }
frlmssuvc1.r ( 𝜑𝑅 ∈ Ring )
frlmssuvc1.i ( 𝜑𝐼𝑉 )
frlmssuvc1.j ( 𝜑𝐽𝐼 )
frlmssuvc1.l ( 𝜑𝐿𝐽 )
frlmssuvc1.x ( 𝜑𝑋𝐾 )
Assertion frlmssuvc1 ( 𝜑 → ( 𝑋 · ( 𝑈𝐿 ) ) ∈ 𝐶 )

### Proof

Step Hyp Ref Expression
1 frlmssuvc1.f 𝐹 = ( 𝑅 freeLMod 𝐼 )
2 frlmssuvc1.u 𝑈 = ( 𝑅 unitVec 𝐼 )
3 frlmssuvc1.b 𝐵 = ( Base ‘ 𝐹 )
4 frlmssuvc1.k 𝐾 = ( Base ‘ 𝑅 )
5 frlmssuvc1.t · = ( ·𝑠𝐹 )
6 frlmssuvc1.z 0 = ( 0g𝑅 )
7 frlmssuvc1.c 𝐶 = { 𝑥𝐵 ∣ ( 𝑥 supp 0 ) ⊆ 𝐽 }
8 frlmssuvc1.r ( 𝜑𝑅 ∈ Ring )
9 frlmssuvc1.i ( 𝜑𝐼𝑉 )
10 frlmssuvc1.j ( 𝜑𝐽𝐼 )
11 frlmssuvc1.l ( 𝜑𝐿𝐽 )
12 frlmssuvc1.x ( 𝜑𝑋𝐾 )
13 1 frlmlmod ( ( 𝑅 ∈ Ring ∧ 𝐼𝑉 ) → 𝐹 ∈ LMod )
14 8 9 13 syl2anc ( 𝜑𝐹 ∈ LMod )
15 eqid ( LSubSp ‘ 𝐹 ) = ( LSubSp ‘ 𝐹 )
16 1 15 3 6 7 frlmsslss2 ( ( 𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼 ) → 𝐶 ∈ ( LSubSp ‘ 𝐹 ) )
17 8 9 10 16 syl3anc ( 𝜑𝐶 ∈ ( LSubSp ‘ 𝐹 ) )
18 1 frlmsca ( ( 𝑅 ∈ Ring ∧ 𝐼𝑉 ) → 𝑅 = ( Scalar ‘ 𝐹 ) )
19 8 9 18 syl2anc ( 𝜑𝑅 = ( Scalar ‘ 𝐹 ) )
20 19 fveq2d ( 𝜑 → ( Base ‘ 𝑅 ) = ( Base ‘ ( Scalar ‘ 𝐹 ) ) )
21 4 20 syl5eq ( 𝜑𝐾 = ( Base ‘ ( Scalar ‘ 𝐹 ) ) )
22 12 21 eleqtrd ( 𝜑𝑋 ∈ ( Base ‘ ( Scalar ‘ 𝐹 ) ) )
23 2 1 3 uvcff ( ( 𝑅 ∈ Ring ∧ 𝐼𝑉 ) → 𝑈 : 𝐼𝐵 )
24 8 9 23 syl2anc ( 𝜑𝑈 : 𝐼𝐵 )
25 10 11 sseldd ( 𝜑𝐿𝐼 )
26 24 25 ffvelrnd ( 𝜑 → ( 𝑈𝐿 ) ∈ 𝐵 )
27 1 4 3 frlmbasf ( ( 𝐼𝑉 ∧ ( 𝑈𝐿 ) ∈ 𝐵 ) → ( 𝑈𝐿 ) : 𝐼𝐾 )
28 9 26 27 syl2anc ( 𝜑 → ( 𝑈𝐿 ) : 𝐼𝐾 )
29 8 adantr ( ( 𝜑𝑥 ∈ ( 𝐼𝐽 ) ) → 𝑅 ∈ Ring )
30 9 adantr ( ( 𝜑𝑥 ∈ ( 𝐼𝐽 ) ) → 𝐼𝑉 )
31 25 adantr ( ( 𝜑𝑥 ∈ ( 𝐼𝐽 ) ) → 𝐿𝐼 )
32 eldifi ( 𝑥 ∈ ( 𝐼𝐽 ) → 𝑥𝐼 )
33 32 adantl ( ( 𝜑𝑥 ∈ ( 𝐼𝐽 ) ) → 𝑥𝐼 )
34 disjdif ( 𝐽 ∩ ( 𝐼𝐽 ) ) = ∅
35 simpr ( ( 𝜑𝑥 ∈ ( 𝐼𝐽 ) ) → 𝑥 ∈ ( 𝐼𝐽 ) )
36 disjne ( ( ( 𝐽 ∩ ( 𝐼𝐽 ) ) = ∅ ∧ 𝐿𝐽𝑥 ∈ ( 𝐼𝐽 ) ) → 𝐿𝑥 )
37 34 11 35 36 mp3an2ani ( ( 𝜑𝑥 ∈ ( 𝐼𝐽 ) ) → 𝐿𝑥 )
38 2 29 30 31 33 37 6 uvcvv0 ( ( 𝜑𝑥 ∈ ( 𝐼𝐽 ) ) → ( ( 𝑈𝐿 ) ‘ 𝑥 ) = 0 )
39 28 38 suppss ( 𝜑 → ( ( 𝑈𝐿 ) supp 0 ) ⊆ 𝐽 )
40 oveq1 ( 𝑥 = ( 𝑈𝐿 ) → ( 𝑥 supp 0 ) = ( ( 𝑈𝐿 ) supp 0 ) )
41 40 sseq1d ( 𝑥 = ( 𝑈𝐿 ) → ( ( 𝑥 supp 0 ) ⊆ 𝐽 ↔ ( ( 𝑈𝐿 ) supp 0 ) ⊆ 𝐽 ) )
42 41 7 elrab2 ( ( 𝑈𝐿 ) ∈ 𝐶 ↔ ( ( 𝑈𝐿 ) ∈ 𝐵 ∧ ( ( 𝑈𝐿 ) supp 0 ) ⊆ 𝐽 ) )
43 26 39 42 sylanbrc ( 𝜑 → ( 𝑈𝐿 ) ∈ 𝐶 )
44 eqid ( Scalar ‘ 𝐹 ) = ( Scalar ‘ 𝐹 )
45 eqid ( Base ‘ ( Scalar ‘ 𝐹 ) ) = ( Base ‘ ( Scalar ‘ 𝐹 ) )
46 44 5 45 15 lssvscl ( ( ( 𝐹 ∈ LMod ∧ 𝐶 ∈ ( LSubSp ‘ 𝐹 ) ) ∧ ( 𝑋 ∈ ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∧ ( 𝑈𝐿 ) ∈ 𝐶 ) ) → ( 𝑋 · ( 𝑈𝐿 ) ) ∈ 𝐶 )
47 14 17 22 43 46 syl22anc ( 𝜑 → ( 𝑋 · ( 𝑈𝐿 ) ) ∈ 𝐶 )