Step | Hyp | Ref
| Expression |
1 | | prdsidlem.z |
. . . 4
⊢ 0 =
(0g ∘ 𝑅) |
2 | | fvex 6113 |
. . . . . 6
⊢ (𝑅‘𝑦) ∈ V |
3 | 2 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → (𝑅‘𝑦) ∈ V) |
4 | | prdsplusgcl.r |
. . . . . 6
⊢ (𝜑 → 𝑅:𝐼⟶Mnd) |
5 | 4 | feqmptd 6159 |
. . . . 5
⊢ (𝜑 → 𝑅 = (𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦))) |
6 | | fn0g 17085 |
. . . . . . 7
⊢
0g Fn V |
7 | 6 | a1i 11 |
. . . . . 6
⊢ (𝜑 → 0g Fn
V) |
8 | | dffn5 6151 |
. . . . . 6
⊢
(0g Fn V ↔ 0g = (𝑥 ∈ V ↦ (0g‘𝑥))) |
9 | 7, 8 | sylib 207 |
. . . . 5
⊢ (𝜑 → 0g = (𝑥 ∈ V ↦
(0g‘𝑥))) |
10 | | fveq2 6103 |
. . . . 5
⊢ (𝑥 = (𝑅‘𝑦) → (0g‘𝑥) = (0g‘(𝑅‘𝑦))) |
11 | 3, 5, 9, 10 | fmptco 6303 |
. . . 4
⊢ (𝜑 → (0g ∘
𝑅) = (𝑦 ∈ 𝐼 ↦ (0g‘(𝑅‘𝑦)))) |
12 | 1, 11 | syl5eq 2656 |
. . 3
⊢ (𝜑 → 0 = (𝑦 ∈ 𝐼 ↦ (0g‘(𝑅‘𝑦)))) |
13 | 4 | ffvelrnda 6267 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → (𝑅‘𝑦) ∈ Mnd) |
14 | | eqid 2610 |
. . . . . . 7
⊢
(Base‘(𝑅‘𝑦)) = (Base‘(𝑅‘𝑦)) |
15 | | eqid 2610 |
. . . . . . 7
⊢
(0g‘(𝑅‘𝑦)) = (0g‘(𝑅‘𝑦)) |
16 | 14, 15 | mndidcl 17131 |
. . . . . 6
⊢ ((𝑅‘𝑦) ∈ Mnd →
(0g‘(𝑅‘𝑦)) ∈ (Base‘(𝑅‘𝑦))) |
17 | 13, 16 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → (0g‘(𝑅‘𝑦)) ∈ (Base‘(𝑅‘𝑦))) |
18 | 17 | ralrimiva 2949 |
. . . 4
⊢ (𝜑 → ∀𝑦 ∈ 𝐼 (0g‘(𝑅‘𝑦)) ∈ (Base‘(𝑅‘𝑦))) |
19 | | prdsplusgcl.y |
. . . . 5
⊢ 𝑌 = (𝑆Xs𝑅) |
20 | | prdsplusgcl.b |
. . . . 5
⊢ 𝐵 = (Base‘𝑌) |
21 | | prdsplusgcl.s |
. . . . 5
⊢ (𝜑 → 𝑆 ∈ 𝑉) |
22 | | prdsplusgcl.i |
. . . . 5
⊢ (𝜑 → 𝐼 ∈ 𝑊) |
23 | | ffn 5958 |
. . . . . 6
⊢ (𝑅:𝐼⟶Mnd → 𝑅 Fn 𝐼) |
24 | 4, 23 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑅 Fn 𝐼) |
25 | 19, 20, 21, 22, 24 | prdsbasmpt 15953 |
. . . 4
⊢ (𝜑 → ((𝑦 ∈ 𝐼 ↦ (0g‘(𝑅‘𝑦))) ∈ 𝐵 ↔ ∀𝑦 ∈ 𝐼 (0g‘(𝑅‘𝑦)) ∈ (Base‘(𝑅‘𝑦)))) |
26 | 18, 25 | mpbird 246 |
. . 3
⊢ (𝜑 → (𝑦 ∈ 𝐼 ↦ (0g‘(𝑅‘𝑦))) ∈ 𝐵) |
27 | 12, 26 | eqeltrd 2688 |
. 2
⊢ (𝜑 → 0 ∈ 𝐵) |
28 | 1 | fveq1i 6104 |
. . . . . . . . . 10
⊢ ( 0 ‘𝑦) = ((0g ∘
𝑅)‘𝑦) |
29 | | fvco2 6183 |
. . . . . . . . . . 11
⊢ ((𝑅 Fn 𝐼 ∧ 𝑦 ∈ 𝐼) → ((0g ∘ 𝑅)‘𝑦) = (0g‘(𝑅‘𝑦))) |
30 | 24, 29 | sylan 487 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → ((0g ∘ 𝑅)‘𝑦) = (0g‘(𝑅‘𝑦))) |
31 | 28, 30 | syl5eq 2656 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → ( 0 ‘𝑦) = (0g‘(𝑅‘𝑦))) |
32 | 31 | adantlr 747 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐼) → ( 0 ‘𝑦) = (0g‘(𝑅‘𝑦))) |
33 | 32 | oveq1d 6564 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐼) → (( 0 ‘𝑦)(+g‘(𝑅‘𝑦))(𝑥‘𝑦)) = ((0g‘(𝑅‘𝑦))(+g‘(𝑅‘𝑦))(𝑥‘𝑦))) |
34 | 4 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝑅:𝐼⟶Mnd) |
35 | 34 | ffvelrnda 6267 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐼) → (𝑅‘𝑦) ∈ Mnd) |
36 | 21 | ad2antrr 758 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐼) → 𝑆 ∈ 𝑉) |
37 | 22 | ad2antrr 758 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐼) → 𝐼 ∈ 𝑊) |
38 | 24 | ad2antrr 758 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐼) → 𝑅 Fn 𝐼) |
39 | | simplr 788 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐼) → 𝑥 ∈ 𝐵) |
40 | | simpr 476 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐼) → 𝑦 ∈ 𝐼) |
41 | 19, 20, 36, 37, 38, 39, 40 | prdsbasprj 15955 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐼) → (𝑥‘𝑦) ∈ (Base‘(𝑅‘𝑦))) |
42 | | eqid 2610 |
. . . . . . . . 9
⊢
(+g‘(𝑅‘𝑦)) = (+g‘(𝑅‘𝑦)) |
43 | 14, 42, 15 | mndlid 17134 |
. . . . . . . 8
⊢ (((𝑅‘𝑦) ∈ Mnd ∧ (𝑥‘𝑦) ∈ (Base‘(𝑅‘𝑦))) → ((0g‘(𝑅‘𝑦))(+g‘(𝑅‘𝑦))(𝑥‘𝑦)) = (𝑥‘𝑦)) |
44 | 35, 41, 43 | syl2anc 691 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐼) → ((0g‘(𝑅‘𝑦))(+g‘(𝑅‘𝑦))(𝑥‘𝑦)) = (𝑥‘𝑦)) |
45 | 33, 44 | eqtrd 2644 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐼) → (( 0 ‘𝑦)(+g‘(𝑅‘𝑦))(𝑥‘𝑦)) = (𝑥‘𝑦)) |
46 | 45 | mpteq2dva 4672 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑦 ∈ 𝐼 ↦ (( 0 ‘𝑦)(+g‘(𝑅‘𝑦))(𝑥‘𝑦))) = (𝑦 ∈ 𝐼 ↦ (𝑥‘𝑦))) |
47 | 21 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝑆 ∈ 𝑉) |
48 | 22 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐼 ∈ 𝑊) |
49 | 24 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝑅 Fn 𝐼) |
50 | 27 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 0 ∈ 𝐵) |
51 | | simpr 476 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝐵) |
52 | | prdsplusgcl.p |
. . . . . 6
⊢ + =
(+g‘𝑌) |
53 | 19, 20, 47, 48, 49, 50, 51, 52 | prdsplusgval 15956 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ( 0 + 𝑥) = (𝑦 ∈ 𝐼 ↦ (( 0 ‘𝑦)(+g‘(𝑅‘𝑦))(𝑥‘𝑦)))) |
54 | 19, 20, 47, 48, 49, 51 | prdsbasfn 15954 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝑥 Fn 𝐼) |
55 | | dffn5 6151 |
. . . . . 6
⊢ (𝑥 Fn 𝐼 ↔ 𝑥 = (𝑦 ∈ 𝐼 ↦ (𝑥‘𝑦))) |
56 | 54, 55 | sylib 207 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝑥 = (𝑦 ∈ 𝐼 ↦ (𝑥‘𝑦))) |
57 | 46, 53, 56 | 3eqtr4d 2654 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ( 0 + 𝑥) = 𝑥) |
58 | 32 | oveq2d 6565 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐼) → ((𝑥‘𝑦)(+g‘(𝑅‘𝑦))( 0 ‘𝑦)) = ((𝑥‘𝑦)(+g‘(𝑅‘𝑦))(0g‘(𝑅‘𝑦)))) |
59 | 14, 42, 15 | mndrid 17135 |
. . . . . . . 8
⊢ (((𝑅‘𝑦) ∈ Mnd ∧ (𝑥‘𝑦) ∈ (Base‘(𝑅‘𝑦))) → ((𝑥‘𝑦)(+g‘(𝑅‘𝑦))(0g‘(𝑅‘𝑦))) = (𝑥‘𝑦)) |
60 | 35, 41, 59 | syl2anc 691 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐼) → ((𝑥‘𝑦)(+g‘(𝑅‘𝑦))(0g‘(𝑅‘𝑦))) = (𝑥‘𝑦)) |
61 | 58, 60 | eqtrd 2644 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐼) → ((𝑥‘𝑦)(+g‘(𝑅‘𝑦))( 0 ‘𝑦)) = (𝑥‘𝑦)) |
62 | 61 | mpteq2dva 4672 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑦 ∈ 𝐼 ↦ ((𝑥‘𝑦)(+g‘(𝑅‘𝑦))( 0 ‘𝑦))) = (𝑦 ∈ 𝐼 ↦ (𝑥‘𝑦))) |
63 | 19, 20, 47, 48, 49, 51, 50, 52 | prdsplusgval 15956 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑥 + 0 ) = (𝑦 ∈ 𝐼 ↦ ((𝑥‘𝑦)(+g‘(𝑅‘𝑦))( 0 ‘𝑦)))) |
64 | 62, 63, 56 | 3eqtr4d 2654 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑥 + 0 ) = 𝑥) |
65 | 57, 64 | jca 553 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (( 0 + 𝑥) = 𝑥 ∧ (𝑥 + 0 ) = 𝑥)) |
66 | 65 | ralrimiva 2949 |
. 2
⊢ (𝜑 → ∀𝑥 ∈ 𝐵 (( 0 + 𝑥) = 𝑥 ∧ (𝑥 + 0 ) = 𝑥)) |
67 | 27, 66 | jca 553 |
1
⊢ (𝜑 → ( 0 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐵 (( 0 + 𝑥) = 𝑥 ∧ (𝑥 + 0 ) = 𝑥))) |