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	$$⊢E=\mathrm{RLReg}\left(R\right)$$
	rrgval.b	$$⊢B={\mathrm{Base}}_R$$
	rrgval.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	rrgval.z	$$⊢\underset{\dot{}}{0}=0_R$$
	rrgsupp.i	$$⊢\phi \to I\in V$$
	rrgsupp.r	$$⊢\phi \to R\in \mathrm{Ring}$$
	rrgsupp.x	$$⊢\phi \to X\in E$$
	rrgsupp.y	$$⊢\phi \to Y:I⟶B$$
Assertion	rrgsupp	$$⊢\phi \to \left(\left(I\times \left\{X\right\}\right){\underset{\dot{}}{·}}_{f}Y\right)\mathrm{supp}\underset{\dot{}}{0}=Y\mathrm{supp}\underset{\dot{}}{0}$$

Proof

Step	Hyp	Ref	Expression
1		rrgval.e	$$⊢E=\mathrm{RLReg}\left(R\right)$$
2		rrgval.b	$$⊢B={\mathrm{Base}}_R$$
3		rrgval.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
4		rrgval.z	$$⊢\underset{\dot{}}{0}=0_R$$
5		rrgsupp.i	$$⊢\phi \to I\in V$$
6		rrgsupp.r	$$⊢\phi \to R\in \mathrm{Ring}$$
7		rrgsupp.x	$$⊢\phi \to X\in E$$
8		rrgsupp.y	$$⊢\phi \to Y:I⟶B$$
9	7	adantr	$$⊢\left(\phi \wedge y\in I\right)\to X\in E$$
10		fvexd	$$⊢\left(\phi \wedge y\in I\right)\to Y\left(y\right)\in \mathrm{V}$$
11		fconstmpt	$$⊢I\times \left\{X\right\}=\left(y\in I⟼X\right)$$
12	11	a1i	$$⊢\phi \to I\times \left\{X\right\}=\left(y\in I⟼X\right)$$
13	8	feqmptd	$$⊢\phi \to Y=\left(y\in I⟼Y\left(y\right)\right)$$
14	5 9 10 12 13	offval2	$$⊢\phi \to \left(I\times \left\{X\right\}\right){\underset{\dot{}}{·}}_{f}Y=\left(y\in I⟼X\underset{\dot{}}{·}Y\left(y\right)\right)$$
15	14	adantr	$$⊢\left(\phi \wedge x\in I\right)\to \left(I\times \left\{X\right\}\right){\underset{\dot{}}{·}}_{f}Y=\left(y\in I⟼X\underset{\dot{}}{·}Y\left(y\right)\right)$$
16	15	fveq1d	$$⊢\left(\phi \wedge x\in I\right)\to \left(\left(I\times \left\{X\right\}\right){\underset{\dot{}}{·}}_{f}Y\right)\left(x\right)=\left(y\in I⟼X\underset{\dot{}}{·}Y\left(y\right)\right)\left(x\right)$$
17		simpr	$$⊢\left(\phi \wedge x\in I\right)\to x\in I$$
18		ovex	$$⊢X\underset{\dot{}}{·}Y\left(x\right)\in \mathrm{V}$$
19		fveq2	$$⊢y=x\to Y\left(y\right)=Y\left(x\right)$$
20	19	oveq2d	$$⊢y=x\to X\underset{\dot{}}{·}Y\left(y\right)=X\underset{\dot{}}{·}Y\left(x\right)$$
21		eqid	$$⊢\left(y\in I⟼X\underset{\dot{}}{·}Y\left(y\right)\right)=\left(y\in I⟼X\underset{\dot{}}{·}Y\left(y\right)\right)$$
22	20 21	fvmptg	$$⊢\left(x\in I\wedge X\underset{\dot{}}{·}Y\left(x\right)\in \mathrm{V}\right)\to \left(y\in I⟼X\underset{\dot{}}{·}Y\left(y\right)\right)\left(x\right)=X\underset{\dot{}}{·}Y\left(x\right)$$
23	17 18 22	sylancl	$$⊢\left(\phi \wedge x\in I\right)\to \left(y\in I⟼X\underset{\dot{}}{·}Y\left(y\right)\right)\left(x\right)=X\underset{\dot{}}{·}Y\left(x\right)$$
24	16 23	eqtrd	$$⊢\left(\phi \wedge x\in I\right)\to \left(\left(I\times \left\{X\right\}\right){\underset{\dot{}}{·}}_{f}Y\right)\left(x\right)=X\underset{\dot{}}{·}Y\left(x\right)$$
25	24	neeq1d	$$⊢\left(\phi \wedge x\in I\right)\to \left(\left(\left(I\times \left\{X\right\}\right){\underset{\dot{}}{·}}_{f}Y\right)\left(x\right)\ne \underset{\dot{}}{0}\leftrightarrow X\underset{\dot{}}{·}Y\left(x\right)\ne \underset{\dot{}}{0}\right)$$
26	25	rabbidva	$$⊢\phi \to \left\{x\in I|\left(\left(I\times \left\{X\right\}\right){\underset{\dot{}}{·}}_{f}Y\right)\left(x\right)\ne \underset{\dot{}}{0}\right\}=\left\{x\in I|X\underset{\dot{}}{·}Y\left(x\right)\ne \underset{\dot{}}{0}\right\}$$
27	6	adantr	$$⊢\left(\phi \wedge x\in I\right)\to R\in \mathrm{Ring}$$
28	7	adantr	$$⊢\left(\phi \wedge x\in I\right)\to X\in E$$
29	8	ffvelrnda	$$⊢\left(\phi \wedge x\in I\right)\to Y\left(x\right)\in B$$
30	1 2 3 4	rrgeq0	$$⊢\left(R\in \mathrm{Ring}\wedge X\in E\wedge Y\left(x\right)\in B\right)\to \left(X\underset{\dot{}}{·}Y\left(x\right)=\underset{\dot{}}{0}\leftrightarrow Y\left(x\right)=\underset{\dot{}}{0}\right)$$
31	27 28 29 30	syl3anc	$$⊢\left(\phi \wedge x\in I\right)\to \left(X\underset{\dot{}}{·}Y\left(x\right)=\underset{\dot{}}{0}\leftrightarrow Y\left(x\right)=\underset{\dot{}}{0}\right)$$
32	31	necon3bid	$$⊢\left(\phi \wedge x\in I\right)\to \left(X\underset{\dot{}}{·}Y\left(x\right)\ne \underset{\dot{}}{0}\leftrightarrow Y\left(x\right)\ne \underset{\dot{}}{0}\right)$$
33	32	rabbidva	$$⊢\phi \to \left\{x\in I|X\underset{\dot{}}{·}Y\left(x\right)\ne \underset{\dot{}}{0}\right\}=\left\{x\in I|Y\left(x\right)\ne \underset{\dot{}}{0}\right\}$$
34	26 33	eqtrd	$$⊢\phi \to \left\{x\in I|\left(\left(I\times \left\{X\right\}\right){\underset{\dot{}}{·}}_{f}Y\right)\left(x\right)\ne \underset{\dot{}}{0}\right\}=\left\{x\in I|Y\left(x\right)\ne \underset{\dot{}}{0}\right\}$$
35		ovex	$$⊢X\underset{\dot{}}{·}Y\left(y\right)\in \mathrm{V}$$
36	35 21	fnmpti	$$⊢\left(y\in I⟼X\underset{\dot{}}{·}Y\left(y\right)\right)FnI$$
37		fneq1	$$⊢\left(I\times \left\{X\right\}\right){\underset{\dot{}}{·}}_{f}Y=\left(y\in I⟼X\underset{\dot{}}{·}Y\left(y\right)\right)\to \left(\left(\left(I\times \left\{X\right\}\right){\underset{\dot{}}{·}}_{f}Y\right)FnI\leftrightarrow \left(y\in I⟼X\underset{\dot{}}{·}Y\left(y\right)\right)FnI\right)$$
38	36 37	mpbiri	$$⊢\left(I\times \left\{X\right\}\right){\underset{\dot{}}{·}}_{f}Y=\left(y\in I⟼X\underset{\dot{}}{·}Y\left(y\right)\right)\to \left(\left(I\times \left\{X\right\}\right){\underset{\dot{}}{·}}_{f}Y\right)FnI$$
39	14 38	syl	$$⊢\phi \to \left(\left(I\times \left\{X\right\}\right){\underset{\dot{}}{·}}_{f}Y\right)FnI$$
40	4	fvexi	$$⊢\underset{\dot{}}{0}\in \mathrm{V}$$
41	40	a1i	$$⊢\phi \to \underset{\dot{}}{0}\in \mathrm{V}$$
42		suppvalfn	$$⊢\left(\left(\left(I\times \left\{X\right\}\right){\underset{\dot{}}{·}}_{f}Y\right)FnI\wedge I\in V\wedge \underset{\dot{}}{0}\in \mathrm{V}\right)\to \left(\left(I\times \left\{X\right\}\right){\underset{\dot{}}{·}}_{f}Y\right)\mathrm{supp}\underset{\dot{}}{0}=\left\{x\in I|\left(\left(I\times \left\{X\right\}\right){\underset{\dot{}}{·}}_{f}Y\right)\left(x\right)\ne \underset{\dot{}}{0}\right\}$$
43	39 5 41 42	syl3anc	$$⊢\phi \to \left(\left(I\times \left\{X\right\}\right){\underset{\dot{}}{·}}_{f}Y\right)\mathrm{supp}\underset{\dot{}}{0}=\left\{x\in I|\left(\left(I\times \left\{X\right\}\right){\underset{\dot{}}{·}}_{f}Y\right)\left(x\right)\ne \underset{\dot{}}{0}\right\}$$
44	8	ffnd	$$⊢\phi \to YFnI$$
45		suppvalfn	$$⊢\left(YFnI\wedge I\in V\wedge \underset{\dot{}}{0}\in \mathrm{V}\right)\to Y\mathrm{supp}\underset{\dot{}}{0}=\left\{x\in I|Y\left(x\right)\ne \underset{\dot{}}{0}\right\}$$
46	44 5 41 45	syl3anc	$$⊢\phi \to Y\mathrm{supp}\underset{\dot{}}{0}=\left\{x\in I|Y\left(x\right)\ne \underset{\dot{}}{0}\right\}$$
47	34 43 46	3eqtr4d	$$⊢\phi \to \left(\left(I\times \left\{X\right\}\right){\underset{\dot{}}{·}}_{f}Y\right)\mathrm{supp}\underset{\dot{}}{0}=Y\mathrm{supp}\underset{\dot{}}{0}$$