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 ) )