prdsidlem

Description: Characterization of identity in a structure product. (Contributed by Mario Carneiro, 10-Jan-2015)

	Ref	Expression
Hypotheses	prdsplusgcl.y	$⊢ Y = S ⨉_{𝑠} R$
	prdsplusgcl.b	$⊢ B = {Base}_{Y}$
	prdsplusgcl.p	$⊢ \underset{˙}{+} = +_{Y}$
	prdsplusgcl.s	$⊢ φ \to S \in V$
	prdsplusgcl.i	$⊢ φ \to I \in W$
	prdsplusgcl.r	$⊢ φ \to R : I ⟶ Mnd$
	prdsidlem.z	$⊢ \underset{˙}{0} = 0_{𝑔} \circ R$
Assertion	prdsidlem	$⊢ φ \to (\underset{˙}{0} \in B \land \forall x \in B (\underset{˙}{0} \underset{˙}{+} x = x \land x \underset{˙}{+} \underset{˙}{0} = x))$

Proof

Step	Hyp	Ref	Expression
1		prdsplusgcl.y	$⊢ Y = S ⨉_{𝑠} R$
2		prdsplusgcl.b	$⊢ B = {Base}_{Y}$
3		prdsplusgcl.p	$⊢ \underset{˙}{+} = +_{Y}$
4		prdsplusgcl.s	$⊢ φ \to S \in V$
5		prdsplusgcl.i	$⊢ φ \to I \in W$
6		prdsplusgcl.r	$⊢ φ \to R : I ⟶ Mnd$
7		prdsidlem.z	$⊢ \underset{˙}{0} = 0_{𝑔} \circ R$
8		fvexd	$⊢ (φ \land y \in I) \to R (y) \in V$
9	6	feqmptd	$⊢ φ \to R = (y \in I ⟼ R (y))$
10		fn0g	$⊢ 0_{𝑔} Fn V$
11	10	a1i	$⊢ φ \to 0_{𝑔} Fn V$
12		dffn5	$⊢ 0_{𝑔} Fn V \leftrightarrow 0_{𝑔} = (x \in V ⟼ 0_{x})$
13	11 12	sylib	$⊢ φ \to 0_{𝑔} = (x \in V ⟼ 0_{x})$
14		fveq2	$⊢ x = R (y) \to 0_{x} = 0_{R (y)}$
15	8 9 13 14	fmptco	$⊢ φ \to 0_{𝑔} \circ R = (y \in I ⟼ 0_{R (y)})$
16	7 15	syl5eq	$⊢ φ \to \underset{˙}{0} = (y \in I ⟼ 0_{R (y)})$
17	6	ffvelrnda	$⊢ (φ \land y \in I) \to R (y) \in Mnd$
18		eqid	$⊢ {Base}_{R (y)} = {Base}_{R (y)}$
19		eqid	$⊢ 0_{R (y)} = 0_{R (y)}$
20	18 19	mndidcl	$⊢ R (y) \in Mnd \to 0_{R (y)} \in {Base}_{R (y)}$
21	17 20	syl	$⊢ (φ \land y \in I) \to 0_{R (y)} \in {Base}_{R (y)}$
22	21	ralrimiva	$⊢ φ \to \forall y \in I 0_{R (y)} \in {Base}_{R (y)}$
23	6	ffnd	$⊢ φ \to R Fn I$
24	1 2 4 5 23	prdsbasmpt	$⊢ φ \to ((y \in I ⟼ 0_{R (y)}) \in B \leftrightarrow \forall y \in I 0_{R (y)} \in {Base}_{R (y)})$
25	22 24	mpbird	$⊢ φ \to (y \in I ⟼ 0_{R (y)}) \in B$
26	16 25	eqeltrd	$⊢ φ \to \underset{˙}{0} \in B$
27	7	fveq1i	$⊢ \underset{˙}{0} (y) = (0_{𝑔} \circ R) (y)$
28		fvco2	$⊢ (R Fn I \land y \in I) \to (0_{𝑔} \circ R) (y) = 0_{R (y)}$
29	23 28	sylan	$⊢ (φ \land y \in I) \to (0_{𝑔} \circ R) (y) = 0_{R (y)}$
30	27 29	syl5eq	$⊢ (φ \land y \in I) \to \underset{˙}{0} (y) = 0_{R (y)}$
31	30	adantlr	$⊢ ((φ \land x \in B) \land y \in I) \to \underset{˙}{0} (y) = 0_{R (y)}$
32	31	oveq1d	$⊢ ((φ \land x \in B) \land y \in I) \to \underset{˙}{0} (y) +_{R (y)} x (y) = 0_{R (y)} +_{R (y)} x (y)$
33	6	adantr	$⊢ (φ \land x \in B) \to R : I ⟶ Mnd$
34	33	ffvelrnda	$⊢ ((φ \land x \in B) \land y \in I) \to R (y) \in Mnd$
35	4	ad2antrr	$⊢ ((φ \land x \in B) \land y \in I) \to S \in V$
36	5	ad2antrr	$⊢ ((φ \land x \in B) \land y \in I) \to I \in W$
37	23	ad2antrr	$⊢ ((φ \land x \in B) \land y \in I) \to R Fn I$
38		simplr	$⊢ ((φ \land x \in B) \land y \in I) \to x \in B$
39		simpr	$⊢ ((φ \land x \in B) \land y \in I) \to y \in I$
40	1 2 35 36 37 38 39	prdsbasprj	$⊢ ((φ \land x \in B) \land y \in I) \to x (y) \in {Base}_{R (y)}$
41		eqid	$⊢ +_{R (y)} = +_{R (y)}$
42	18 41 19	mndlid	$⊢ (R (y) \in Mnd \land x (y) \in {Base}_{R (y)}) \to 0_{R (y)} +_{R (y)} x (y) = x (y)$
43	34 40 42	syl2anc	$⊢ ((φ \land x \in B) \land y \in I) \to 0_{R (y)} +_{R (y)} x (y) = x (y)$
44	32 43	eqtrd	$⊢ ((φ \land x \in B) \land y \in I) \to \underset{˙}{0} (y) +_{R (y)} x (y) = x (y)$
45	44	mpteq2dva	$⊢ (φ \land x \in B) \to (y \in I ⟼ \underset{˙}{0} (y) +_{R (y)} x (y)) = (y \in I ⟼ x (y))$
46	4	adantr	$⊢ (φ \land x \in B) \to S \in V$
47	5	adantr	$⊢ (φ \land x \in B) \to I \in W$
48	23	adantr	$⊢ (φ \land x \in B) \to R Fn I$
49	26	adantr	$⊢ (φ \land x \in B) \to \underset{˙}{0} \in B$
50		simpr	$⊢ (φ \land x \in B) \to x \in B$
51	1 2 46 47 48 49 50 3	prdsplusgval	$⊢ (φ \land x \in B) \to \underset{˙}{0} \underset{˙}{+} x = (y \in I ⟼ \underset{˙}{0} (y) +_{R (y)} x (y))$
52	1 2 46 47 48 50	prdsbasfn	$⊢ (φ \land x \in B) \to x Fn I$
53		dffn5	$⊢ x Fn I \leftrightarrow x = (y \in I ⟼ x (y))$
54	52 53	sylib	$⊢ (φ \land x \in B) \to x = (y \in I ⟼ x (y))$
55	45 51 54	3eqtr4d	$⊢ (φ \land x \in B) \to \underset{˙}{0} \underset{˙}{+} x = x$
56	31	oveq2d	$⊢ ((φ \land x \in B) \land y \in I) \to x (y) +_{R (y)} \underset{˙}{0} (y) = x (y) +_{R (y)} 0_{R (y)}$
57	18 41 19	mndrid	$⊢ (R (y) \in Mnd \land x (y) \in {Base}_{R (y)}) \to x (y) +_{R (y)} 0_{R (y)} = x (y)$
58	34 40 57	syl2anc	$⊢ ((φ \land x \in B) \land y \in I) \to x (y) +_{R (y)} 0_{R (y)} = x (y)$
59	56 58	eqtrd	$⊢ ((φ \land x \in B) \land y \in I) \to x (y) +_{R (y)} \underset{˙}{0} (y) = x (y)$
60	59	mpteq2dva	$⊢ (φ \land x \in B) \to (y \in I ⟼ x (y) +_{R (y)} \underset{˙}{0} (y)) = (y \in I ⟼ x (y))$
61	1 2 46 47 48 50 49 3	prdsplusgval	$⊢ (φ \land x \in B) \to x \underset{˙}{+} \underset{˙}{0} = (y \in I ⟼ x (y) +_{R (y)} \underset{˙}{0} (y))$
62	60 61 54	3eqtr4d	$⊢ (φ \land x \in B) \to x \underset{˙}{+} \underset{˙}{0} = x$
63	55 62	jca	$⊢ (φ \land x \in B) \to (\underset{˙}{0} \underset{˙}{+} x = x \land x \underset{˙}{+} \underset{˙}{0} = x)$
64	63	ralrimiva	$⊢ φ \to \forall x \in B (\underset{˙}{0} \underset{˙}{+} x = x \land x \underset{˙}{+} \underset{˙}{0} = x)$
65	26 64	jca	$⊢ φ \to (\underset{˙}{0} \in B \land \forall x \in B (\underset{˙}{0} \underset{˙}{+} x = x \land x \underset{˙}{+} \underset{˙}{0} = x))$

Metamath Proof Explorer

Theorem prdsidlem

Proof