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

Proof

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

Metamath Proof Explorer

Theorem rrgsupp

Proof