Theorem prdsidlem

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

	Ref	Expression
Hypotheses	prdsplusgcl.y	⊢ 𝑌 = ( 𝑆 Xs 𝑅 )
	prdsplusgcl.b	⊢ 𝐵 = ( Base ‘ 𝑌 )
	prdsplusgcl.p	⊢ + = ( +g ‘ 𝑌 )
	prdsplusgcl.s	⊢ ( 𝜑 → 𝑆 ∈ 𝑉 )
	prdsplusgcl.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
	prdsplusgcl.r	⊢ ( 𝜑 → 𝑅 : 𝐼 ⟶ Mnd )
	prdsidlem.z	⊢ 0 = ( 0g ∘ 𝑅 )
Assertion	prdsidlem	⊢ ( 𝜑 → ( 0 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ( ( 0 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 0 ) = 𝑥 ) ) )

Proof

Step	Hyp	Ref	Expression
1		prdsplusgcl.y	⊢ 𝑌 = ( 𝑆 Xs 𝑅 )
2		prdsplusgcl.b	⊢ 𝐵 = ( Base ‘ 𝑌 )
3		prdsplusgcl.p	⊢ + = ( +g ‘ 𝑌 )
4		prdsplusgcl.s	⊢ ( 𝜑 → 𝑆 ∈ 𝑉 )
5		prdsplusgcl.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
6		prdsplusgcl.r	⊢ ( 𝜑 → 𝑅 : 𝐼 ⟶ Mnd )
7		prdsidlem.z	⊢ 0 = ( 0g ∘ 𝑅 )
8		fvexd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐼 ) → ( 𝑅 ‘ 𝑦 ) ∈ V )
9	6	feqmptd	⊢ ( 𝜑 → 𝑅 = ( 𝑦 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑦 ) ) )
10		fn0g	⊢ 0g Fn V
11	10	a1i	⊢ ( 𝜑 → 0g Fn V )
12		dffn5	⊢ ( 0g Fn V ↔ 0g = ( 𝑥 ∈ V ↦ ( 0g ‘ 𝑥 ) ) )
13	11 12	sylib	⊢ ( 𝜑 → 0g = ( 𝑥 ∈ V ↦ ( 0g ‘ 𝑥 ) ) )
14		fveq2	⊢ ( 𝑥 = ( 𝑅 ‘ 𝑦 ) → ( 0g ‘ 𝑥 ) = ( 0g ‘ ( 𝑅 ‘ 𝑦 ) ) )
15	8 9 13 14	fmptco	⊢ ( 𝜑 → ( 0g ∘ 𝑅 ) = ( 𝑦 ∈ 𝐼 ↦ ( 0g ‘ ( 𝑅 ‘ 𝑦 ) ) ) )
16	7 15	syl5eq	⊢ ( 𝜑 → 0 = ( 𝑦 ∈ 𝐼 ↦ ( 0g ‘ ( 𝑅 ‘ 𝑦 ) ) ) )
17	6	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐼 ) → ( 𝑅 ‘ 𝑦 ) ∈ Mnd )
18		eqid	⊢ ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) = ( Base ‘ ( 𝑅 ‘ 𝑦 ) )
19		eqid	⊢ ( 0g ‘ ( 𝑅 ‘ 𝑦 ) ) = ( 0g ‘ ( 𝑅 ‘ 𝑦 ) )
20	18 19	mndidcl	⊢ ( ( 𝑅 ‘ 𝑦 ) ∈ Mnd → ( 0g ‘ ( 𝑅 ‘ 𝑦 ) ) ∈ ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) )
21	17 20	syl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐼 ) → ( 0g ‘ ( 𝑅 ‘ 𝑦 ) ) ∈ ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) )
22	21	ralrimiva	⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝐼 ( 0g ‘ ( 𝑅 ‘ 𝑦 ) ) ∈ ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) )
23	6	ffnd	⊢ ( 𝜑 → 𝑅 Fn 𝐼 )
24	1 2 4 5 23	prdsbasmpt	⊢ ( 𝜑 → ( ( 𝑦 ∈ 𝐼 ↦ ( 0g ‘ ( 𝑅 ‘ 𝑦 ) ) ) ∈ 𝐵 ↔ ∀ 𝑦 ∈ 𝐼 ( 0g ‘ ( 𝑅 ‘ 𝑦 ) ) ∈ ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) ) )
25	22 24	mpbird	⊢ ( 𝜑 → ( 𝑦 ∈ 𝐼 ↦ ( 0g ‘ ( 𝑅 ‘ 𝑦 ) ) ) ∈ 𝐵 )
26	16 25	eqeltrd	⊢ ( 𝜑 → 0 ∈ 𝐵 )
27	7	fveq1i	⊢ ( 0 ‘ 𝑦 ) = ( ( 0g ∘ 𝑅 ) ‘ 𝑦 )
28		fvco2	⊢ ( ( 𝑅 Fn 𝐼 ∧ 𝑦 ∈ 𝐼 ) → ( ( 0g ∘ 𝑅 ) ‘ 𝑦 ) = ( 0g ‘ ( 𝑅 ‘ 𝑦 ) ) )
29	23 28	sylan	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐼 ) → ( ( 0g ∘ 𝑅 ) ‘ 𝑦 ) = ( 0g ‘ ( 𝑅 ‘ 𝑦 ) ) )
30	27 29	syl5eq	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐼 ) → ( 0 ‘ 𝑦 ) = ( 0g ‘ ( 𝑅 ‘ 𝑦 ) ) )
31	30	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐼 ) → ( 0 ‘ 𝑦 ) = ( 0g ‘ ( 𝑅 ‘ 𝑦 ) ) )
32	31	oveq1d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐼 ) → ( ( 0 ‘ 𝑦 ) ( +g ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑥 ‘ 𝑦 ) ) = ( ( 0g ‘ ( 𝑅 ‘ 𝑦 ) ) ( +g ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑥 ‘ 𝑦 ) ) )
33	6	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝑅 : 𝐼 ⟶ Mnd )
34	33	ffvelrnda	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐼 ) → ( 𝑅 ‘ 𝑦 ) ∈ Mnd )
35	4	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐼 ) → 𝑆 ∈ 𝑉 )
36	5	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐼 ) → 𝐼 ∈ 𝑊 )
37	23	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐼 ) → 𝑅 Fn 𝐼 )
38		simplr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐼 ) → 𝑥 ∈ 𝐵 )
39		simpr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐼 ) → 𝑦 ∈ 𝐼 )
40	1 2 35 36 37 38 39	prdsbasprj	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐼 ) → ( 𝑥 ‘ 𝑦 ) ∈ ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) )
41		eqid	⊢ ( +g ‘ ( 𝑅 ‘ 𝑦 ) ) = ( +g ‘ ( 𝑅 ‘ 𝑦 ) )
42	18 41 19	mndlid	⊢ ( ( ( 𝑅 ‘ 𝑦 ) ∈ Mnd ∧ ( 𝑥 ‘ 𝑦 ) ∈ ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) ) → ( ( 0g ‘ ( 𝑅 ‘ 𝑦 ) ) ( +g ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑥 ‘ 𝑦 ) ) = ( 𝑥 ‘ 𝑦 ) )
43	34 40 42	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐼 ) → ( ( 0g ‘ ( 𝑅 ‘ 𝑦 ) ) ( +g ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑥 ‘ 𝑦 ) ) = ( 𝑥 ‘ 𝑦 ) )
44	32 43	eqtrd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐼 ) → ( ( 0 ‘ 𝑦 ) ( +g ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑥 ‘ 𝑦 ) ) = ( 𝑥 ‘ 𝑦 ) )
45	44	mpteq2dva	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑦 ∈ 𝐼 ↦ ( ( 0 ‘ 𝑦 ) ( +g ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑥 ‘ 𝑦 ) ) ) = ( 𝑦 ∈ 𝐼 ↦ ( 𝑥 ‘ 𝑦 ) ) )
46	4	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝑆 ∈ 𝑉 )
47	5	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝐼 ∈ 𝑊 )
48	23	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝑅 Fn 𝐼 )
49	26	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 0 ∈ 𝐵 )
50		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ 𝐵 )
51	1 2 46 47 48 49 50 3	prdsplusgval	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 0 + 𝑥 ) = ( 𝑦 ∈ 𝐼 ↦ ( ( 0 ‘ 𝑦 ) ( +g ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑥 ‘ 𝑦 ) ) ) )
52	1 2 46 47 48 50	prdsbasfn	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝑥 Fn 𝐼 )
53		dffn5	⊢ ( 𝑥 Fn 𝐼 ↔ 𝑥 = ( 𝑦 ∈ 𝐼 ↦ ( 𝑥 ‘ 𝑦 ) ) )
54	52 53	sylib	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝑥 = ( 𝑦 ∈ 𝐼 ↦ ( 𝑥 ‘ 𝑦 ) ) )
55	45 51 54	3eqtr4d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 0 + 𝑥 ) = 𝑥 )
56	31	oveq2d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐼 ) → ( ( 𝑥 ‘ 𝑦 ) ( +g ‘ ( 𝑅 ‘ 𝑦 ) ) ( 0 ‘ 𝑦 ) ) = ( ( 𝑥 ‘ 𝑦 ) ( +g ‘ ( 𝑅 ‘ 𝑦 ) ) ( 0g ‘ ( 𝑅 ‘ 𝑦 ) ) ) )
57	18 41 19	mndrid	⊢ ( ( ( 𝑅 ‘ 𝑦 ) ∈ Mnd ∧ ( 𝑥 ‘ 𝑦 ) ∈ ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) ) → ( ( 𝑥 ‘ 𝑦 ) ( +g ‘ ( 𝑅 ‘ 𝑦 ) ) ( 0g ‘ ( 𝑅 ‘ 𝑦 ) ) ) = ( 𝑥 ‘ 𝑦 ) )
58	34 40 57	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐼 ) → ( ( 𝑥 ‘ 𝑦 ) ( +g ‘ ( 𝑅 ‘ 𝑦 ) ) ( 0g ‘ ( 𝑅 ‘ 𝑦 ) ) ) = ( 𝑥 ‘ 𝑦 ) )
59	56 58	eqtrd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐼 ) → ( ( 𝑥 ‘ 𝑦 ) ( +g ‘ ( 𝑅 ‘ 𝑦 ) ) ( 0 ‘ 𝑦 ) ) = ( 𝑥 ‘ 𝑦 ) )
60	59	mpteq2dva	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑥 ‘ 𝑦 ) ( +g ‘ ( 𝑅 ‘ 𝑦 ) ) ( 0 ‘ 𝑦 ) ) ) = ( 𝑦 ∈ 𝐼 ↦ ( 𝑥 ‘ 𝑦 ) ) )
61	1 2 46 47 48 50 49 3	prdsplusgval	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 + 0 ) = ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑥 ‘ 𝑦 ) ( +g ‘ ( 𝑅 ‘ 𝑦 ) ) ( 0 ‘ 𝑦 ) ) ) )
62	60 61 54	3eqtr4d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 + 0 ) = 𝑥 )
63	55 62	jca	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( ( 0 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 0 ) = 𝑥 ) )
64	63	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ( ( 0 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 0 ) = 𝑥 ) )
65	26 64	jca	⊢ ( 𝜑 → ( 0 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ( ( 0 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 0 ) = 𝑥 ) ) )