This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 eqtrid ⊢ ( 𝜑 → 0 = ( 𝑦 ∈ 𝐼 ↦ ( 0g ‘ ( 𝑅 ‘ 𝑦 ) ) ) )
17 6 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐼 ) → ( 𝑅 ‘ 𝑦 ) ∈ 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 eqtrid ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐼 ) → ( 0 ‘ 𝑦 ) = ( 0g ‘ ( 𝑅 ‘ 𝑦 ) ) )
31 30 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐼 ) → ( 0 ‘ 𝑦 ) = ( 0g ‘ ( 𝑅 ‘ 𝑦 ) ) )
32 31 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐼 ) → ( ( 0 ‘ 𝑦 ) ( +g ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑥 ‘ 𝑦 ) ) = ( ( 0g ‘ ( 𝑅 ‘ 𝑦 ) ) ( +g ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑥 ‘ 𝑦 ) ) )
33 6 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝑅 : 𝐼 ⟶ Mnd )
34 33 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐼 ) → ( 𝑅 ‘ 𝑦 ) ∈ 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 ) = 𝑥 ) ) )