Metamath Proof Explorer

Theorem rrgsupp

Description: Left multiplication by a left regular element does not change the support set of a vector. (Contributed by Stefan O'Rear, 28-Mar-2015) (Revised by AV, 20-Jul-2019)

Ref Expression
Hypotheses rrgval.e ⊢ 𝐸 = ( RLReg ‘ 𝑅 )
rrgval.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
rrgval.t ⊢ · = ( .r ‘ 𝑅 )
rrgval.z ⊢ 0 = ( 0g ‘ 𝑅 )
rrgsupp.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
rrgsupp.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
rrgsupp.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐸 )
rrgsupp.y ⊢ ( 𝜑 → 𝑌 : 𝐼 ⟶ 𝐵 )
Assertion rrgsupp ( 𝜑 → ( ( ( 𝐼 × { 𝑋 } ) ∘f · 𝑌 ) supp 0 ) = ( 𝑌 supp 0 ) )

Proof

Step Hyp Ref Expression
1 rrgval.e ⊢ 𝐸 = ( RLReg ‘ 𝑅 )
2 rrgval.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
3 rrgval.t ⊢ · = ( .r ‘ 𝑅 )
4 rrgval.z ⊢ 0 = ( 0g ‘ 𝑅 )
5 rrgsupp.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
6 rrgsupp.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
7 rrgsupp.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐸 )
8 rrgsupp.y ⊢ ( 𝜑 → 𝑌 : 𝐼 ⟶ 𝐵 )
9 7 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐼 ) → 𝑋 ∈ 𝐸 )
10 fvexd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐼 ) → ( 𝑌 ‘ 𝑦 ) ∈ V )
11 fconstmpt ⊢ ( 𝐼 × { 𝑋 } ) = ( 𝑦 ∈ 𝐼 ↦ 𝑋 )
12 11 a1i ⊢ ( 𝜑 → ( 𝐼 × { 𝑋 } ) = ( 𝑦 ∈ 𝐼 ↦ 𝑋 ) )
13 8 feqmptd ⊢ ( 𝜑 → 𝑌 = ( 𝑦 ∈ 𝐼 ↦ ( 𝑌 ‘ 𝑦 ) ) )
14 5 9 10 12 13 offval2 ⊢ ( 𝜑 → ( ( 𝐼 × { 𝑋 } ) ∘f · 𝑌 ) = ( 𝑦 ∈ 𝐼 ↦ ( 𝑋 · ( 𝑌 ‘ 𝑦 ) ) ) )
15 14 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝐼 × { 𝑋 } ) ∘f · 𝑌 ) = ( 𝑦 ∈ 𝐼 ↦ ( 𝑋 · ( 𝑌 ‘ 𝑦 ) ) ) )
16 15 fveq1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( ( ( 𝐼 × { 𝑋 } ) ∘f · 𝑌 ) ‘ 𝑥 ) = ( ( 𝑦 ∈ 𝐼 ↦ ( 𝑋 · ( 𝑌 ‘ 𝑦 ) ) ) ‘ 𝑥 ) )
17 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝑥 ∈ 𝐼 )
18 ovex ⊢ ( 𝑋 · ( 𝑌 ‘ 𝑥 ) ) ∈ V
19 fveq2 ⊢ ( 𝑦 = 𝑥 → ( 𝑌 ‘ 𝑦 ) = ( 𝑌 ‘ 𝑥 ) )
20 19 oveq2d ⊢ ( 𝑦 = 𝑥 → ( 𝑋 · ( 𝑌 ‘ 𝑦 ) ) = ( 𝑋 · ( 𝑌 ‘ 𝑥 ) ) )
21 eqid ⊢ ( 𝑦 ∈ 𝐼 ↦ ( 𝑋 · ( 𝑌 ‘ 𝑦 ) ) ) = ( 𝑦 ∈ 𝐼 ↦ ( 𝑋 · ( 𝑌 ‘ 𝑦 ) ) )
22 20 21 fvmptg ⊢ ( ( 𝑥 ∈ 𝐼 ∧ ( 𝑋 · ( 𝑌 ‘ 𝑥 ) ) ∈ V ) → ( ( 𝑦 ∈ 𝐼 ↦ ( 𝑋 · ( 𝑌 ‘ 𝑦 ) ) ) ‘ 𝑥 ) = ( 𝑋 · ( 𝑌 ‘ 𝑥 ) ) )
23 17 18 22 sylancl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝑦 ∈ 𝐼 ↦ ( 𝑋 · ( 𝑌 ‘ 𝑦 ) ) ) ‘ 𝑥 ) = ( 𝑋 · ( 𝑌 ‘ 𝑥 ) ) )
24 16 23 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( ( ( 𝐼 × { 𝑋 } ) ∘f · 𝑌 ) ‘ 𝑥 ) = ( 𝑋 · ( 𝑌 ‘ 𝑥 ) ) )
25 24 neeq1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( ( ( ( 𝐼 × { 𝑋 } ) ∘f · 𝑌 ) ‘ 𝑥 ) ≠ 0 ↔ ( 𝑋 · ( 𝑌 ‘ 𝑥 ) ) ≠ 0 ) )
26 25 rabbidva ⊢ ( 𝜑 → { 𝑥 ∈ 𝐼 ∣ ( ( ( 𝐼 × { 𝑋 } ) ∘f · 𝑌 ) ‘ 𝑥 ) ≠ 0 } = { 𝑥 ∈ 𝐼 ∣ ( 𝑋 · ( 𝑌 ‘ 𝑥 ) ) ≠ 0 } )
27 6 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝑅 ∈ Ring )
28 7 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝑋 ∈ 𝐸 )
29 8 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( 𝑌 ‘ 𝑥 ) ∈ 𝐵 )
30 1 2 3 4 rrgeq0 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐸 ∧ ( 𝑌 ‘ 𝑥 ) ∈ 𝐵 ) → ( ( 𝑋 · ( 𝑌 ‘ 𝑥 ) ) = 0 ↔ ( 𝑌 ‘ 𝑥 ) = 0 ) )
31 27 28 29 30 syl3anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝑋 · ( 𝑌 ‘ 𝑥 ) ) = 0 ↔ ( 𝑌 ‘ 𝑥 ) = 0 ) )
32 31 necon3bid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝑋 · ( 𝑌 ‘ 𝑥 ) ) ≠ 0 ↔ ( 𝑌 ‘ 𝑥 ) ≠ 0 ) )
33 32 rabbidva ⊢ ( 𝜑 → { 𝑥 ∈ 𝐼 ∣ ( 𝑋 · ( 𝑌 ‘ 𝑥 ) ) ≠ 0 } = { 𝑥 ∈ 𝐼 ∣ ( 𝑌 ‘ 𝑥 ) ≠ 0 } )
34 26 33 eqtrd ⊢ ( 𝜑 → { 𝑥 ∈ 𝐼 ∣ ( ( ( 𝐼 × { 𝑋 } ) ∘f · 𝑌 ) ‘ 𝑥 ) ≠ 0 } = { 𝑥 ∈ 𝐼 ∣ ( 𝑌 ‘ 𝑥 ) ≠ 0 } )
35 ovex ⊢ ( 𝑋 · ( 𝑌 ‘ 𝑦 ) ) ∈ V
36 35 21 fnmpti ⊢ ( 𝑦 ∈ 𝐼 ↦ ( 𝑋 · ( 𝑌 ‘ 𝑦 ) ) ) Fn 𝐼
37 fneq1 ⊢ ( ( ( 𝐼 × { 𝑋 } ) ∘f · 𝑌 ) = ( 𝑦 ∈ 𝐼 ↦ ( 𝑋 · ( 𝑌 ‘ 𝑦 ) ) ) → ( ( ( 𝐼 × { 𝑋 } ) ∘f · 𝑌 ) Fn 𝐼 ↔ ( 𝑦 ∈ 𝐼 ↦ ( 𝑋 · ( 𝑌 ‘ 𝑦 ) ) ) Fn 𝐼 ) )
38 36 37 mpbiri ⊢ ( ( ( 𝐼 × { 𝑋 } ) ∘f · 𝑌 ) = ( 𝑦 ∈ 𝐼 ↦ ( 𝑋 · ( 𝑌 ‘ 𝑦 ) ) ) → ( ( 𝐼 × { 𝑋 } ) ∘f · 𝑌 ) Fn 𝐼 )
39 14 38 syl ⊢ ( 𝜑 → ( ( 𝐼 × { 𝑋 } ) ∘f · 𝑌 ) Fn 𝐼 )
40 4 fvexi ⊢ 0 ∈ V
41 40 a1i ⊢ ( 𝜑 → 0 ∈ V )
42 suppvalfn ⊢ ( ( ( ( 𝐼 × { 𝑋 } ) ∘f · 𝑌 ) Fn 𝐼 ∧ 𝐼 ∈ 𝑉 ∧ 0 ∈ V ) → ( ( ( 𝐼 × { 𝑋 } ) ∘f · 𝑌 ) supp 0 ) = { 𝑥 ∈ 𝐼 ∣ ( ( ( 𝐼 × { 𝑋 } ) ∘f · 𝑌 ) ‘ 𝑥 ) ≠ 0 } )
43 39 5 41 42 syl3anc ⊢ ( 𝜑 → ( ( ( 𝐼 × { 𝑋 } ) ∘f · 𝑌 ) supp 0 ) = { 𝑥 ∈ 𝐼 ∣ ( ( ( 𝐼 × { 𝑋 } ) ∘f · 𝑌 ) ‘ 𝑥 ) ≠ 0 } )
44 8 ffnd ⊢ ( 𝜑 → 𝑌 Fn 𝐼 )
45 suppvalfn ⊢ ( ( 𝑌 Fn 𝐼 ∧ 𝐼 ∈ 𝑉 ∧ 0 ∈ V ) → ( 𝑌 supp 0 ) = { 𝑥 ∈ 𝐼 ∣ ( 𝑌 ‘ 𝑥 ) ≠ 0 } )
46 44 5 41 45 syl3anc ⊢ ( 𝜑 → ( 𝑌 supp 0 ) = { 𝑥 ∈ 𝐼 ∣ ( 𝑌 ‘ 𝑥 ) ≠ 0 } )
47 34 43 46 3eqtr4d ⊢ ( 𝜑 → ( ( ( 𝐼 × { 𝑋 } ) ∘f · 𝑌 ) supp 0 ) = ( 𝑌 supp 0 ) )