Step | Hyp | Ref
| Expression |
1 | | eqidd 2623 |
. 2
⊢ (𝜑 → (Base‘𝑌) = (Base‘𝑌)) |
2 | | eqidd 2623 |
. 2
⊢ (𝜑 → (+g‘𝑌) = (+g‘𝑌)) |
3 | | prdsmndd.y |
. . . 4
⊢ 𝑌 = (𝑆Xs𝑅) |
4 | | eqid 2622 |
. . . 4
⊢
(Base‘𝑌) =
(Base‘𝑌) |
5 | | eqid 2622 |
. . . 4
⊢
(+g‘𝑌) = (+g‘𝑌) |
6 | | prdsmndd.s |
. . . . . 6
⊢ (𝜑 → 𝑆 ∈ 𝑉) |
7 | | elex 3212 |
. . . . . 6
⊢ (𝑆 ∈ 𝑉 → 𝑆 ∈ V) |
8 | 6, 7 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑆 ∈ V) |
9 | 8 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑌) ∧ 𝑏 ∈ (Base‘𝑌))) → 𝑆 ∈ V) |
10 | | prdsmndd.i |
. . . . . 6
⊢ (𝜑 → 𝐼 ∈ 𝑊) |
11 | | elex 3212 |
. . . . . 6
⊢ (𝐼 ∈ 𝑊 → 𝐼 ∈ V) |
12 | 10, 11 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝐼 ∈ V) |
13 | 12 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑌) ∧ 𝑏 ∈ (Base‘𝑌))) → 𝐼 ∈ V) |
14 | | prdsmndd.r |
. . . . 5
⊢ (𝜑 → 𝑅:𝐼⟶Mnd) |
15 | 14 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑌) ∧ 𝑏 ∈ (Base‘𝑌))) → 𝑅:𝐼⟶Mnd) |
16 | | simprl 794 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑌) ∧ 𝑏 ∈ (Base‘𝑌))) → 𝑎 ∈ (Base‘𝑌)) |
17 | | simprr 796 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑌) ∧ 𝑏 ∈ (Base‘𝑌))) → 𝑏 ∈ (Base‘𝑌)) |
18 | 3, 4, 5, 9, 13, 15, 16, 17 | prdsplusgcl 17321 |
. . 3
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑌) ∧ 𝑏 ∈ (Base‘𝑌))) → (𝑎(+g‘𝑌)𝑏) ∈ (Base‘𝑌)) |
19 | 18 | 3impb 1260 |
. 2
⊢ ((𝜑 ∧ 𝑎 ∈ (Base‘𝑌) ∧ 𝑏 ∈ (Base‘𝑌)) → (𝑎(+g‘𝑌)𝑏) ∈ (Base‘𝑌)) |
20 | 14 | ffvelrnda 6359 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → (𝑅‘𝑦) ∈ Mnd) |
21 | 20 | adantlr 751 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑌) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → (𝑅‘𝑦) ∈ Mnd) |
22 | 8 | ad2antrr 762 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑌) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → 𝑆 ∈ V) |
23 | 12 | ad2antrr 762 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑌) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → 𝐼 ∈ V) |
24 | | ffn 6045 |
. . . . . . . . 9
⊢ (𝑅:𝐼⟶Mnd → 𝑅 Fn 𝐼) |
25 | 14, 24 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑅 Fn 𝐼) |
26 | 25 | ad2antrr 762 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑌) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → 𝑅 Fn 𝐼) |
27 | | simplr1 1103 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑌) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → 𝑎 ∈ (Base‘𝑌)) |
28 | | simpr 477 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑌) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → 𝑦 ∈ 𝐼) |
29 | 3, 4, 22, 23, 26, 27, 28 | prdsbasprj 16132 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑌) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → (𝑎‘𝑦) ∈ (Base‘(𝑅‘𝑦))) |
30 | | simplr2 1104 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑌) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → 𝑏 ∈ (Base‘𝑌)) |
31 | 3, 4, 22, 23, 26, 30, 28 | prdsbasprj 16132 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑌) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → (𝑏‘𝑦) ∈ (Base‘(𝑅‘𝑦))) |
32 | | simplr3 1105 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑌) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → 𝑐 ∈ (Base‘𝑌)) |
33 | 3, 4, 22, 23, 26, 32, 28 | prdsbasprj 16132 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑌) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → (𝑐‘𝑦) ∈ (Base‘(𝑅‘𝑦))) |
34 | | eqid 2622 |
. . . . . . 7
⊢
(Base‘(𝑅‘𝑦)) = (Base‘(𝑅‘𝑦)) |
35 | | eqid 2622 |
. . . . . . 7
⊢
(+g‘(𝑅‘𝑦)) = (+g‘(𝑅‘𝑦)) |
36 | 34, 35 | mndass 17302 |
. . . . . 6
⊢ (((𝑅‘𝑦) ∈ Mnd ∧ ((𝑎‘𝑦) ∈ (Base‘(𝑅‘𝑦)) ∧ (𝑏‘𝑦) ∈ (Base‘(𝑅‘𝑦)) ∧ (𝑐‘𝑦) ∈ (Base‘(𝑅‘𝑦)))) → (((𝑎‘𝑦)(+g‘(𝑅‘𝑦))(𝑏‘𝑦))(+g‘(𝑅‘𝑦))(𝑐‘𝑦)) = ((𝑎‘𝑦)(+g‘(𝑅‘𝑦))((𝑏‘𝑦)(+g‘(𝑅‘𝑦))(𝑐‘𝑦)))) |
37 | 21, 29, 31, 33, 36 | syl13anc 1328 |
. . . . 5
⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑌) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → (((𝑎‘𝑦)(+g‘(𝑅‘𝑦))(𝑏‘𝑦))(+g‘(𝑅‘𝑦))(𝑐‘𝑦)) = ((𝑎‘𝑦)(+g‘(𝑅‘𝑦))((𝑏‘𝑦)(+g‘(𝑅‘𝑦))(𝑐‘𝑦)))) |
38 | 3, 4, 22, 23, 26, 27, 30, 5, 28 | prdsplusgfval 16134 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑌) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → ((𝑎(+g‘𝑌)𝑏)‘𝑦) = ((𝑎‘𝑦)(+g‘(𝑅‘𝑦))(𝑏‘𝑦))) |
39 | 38 | oveq1d 6665 |
. . . . 5
⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑌) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → (((𝑎(+g‘𝑌)𝑏)‘𝑦)(+g‘(𝑅‘𝑦))(𝑐‘𝑦)) = (((𝑎‘𝑦)(+g‘(𝑅‘𝑦))(𝑏‘𝑦))(+g‘(𝑅‘𝑦))(𝑐‘𝑦))) |
40 | 3, 4, 22, 23, 26, 30, 32, 5, 28 | prdsplusgfval 16134 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑌) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → ((𝑏(+g‘𝑌)𝑐)‘𝑦) = ((𝑏‘𝑦)(+g‘(𝑅‘𝑦))(𝑐‘𝑦))) |
41 | 40 | oveq2d 6666 |
. . . . 5
⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑌) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → ((𝑎‘𝑦)(+g‘(𝑅‘𝑦))((𝑏(+g‘𝑌)𝑐)‘𝑦)) = ((𝑎‘𝑦)(+g‘(𝑅‘𝑦))((𝑏‘𝑦)(+g‘(𝑅‘𝑦))(𝑐‘𝑦)))) |
42 | 37, 39, 41 | 3eqtr4d 2666 |
. . . 4
⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑌) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → (((𝑎(+g‘𝑌)𝑏)‘𝑦)(+g‘(𝑅‘𝑦))(𝑐‘𝑦)) = ((𝑎‘𝑦)(+g‘(𝑅‘𝑦))((𝑏(+g‘𝑌)𝑐)‘𝑦))) |
43 | 42 | mpteq2dva 4744 |
. . 3
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑌) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) → (𝑦 ∈ 𝐼 ↦ (((𝑎(+g‘𝑌)𝑏)‘𝑦)(+g‘(𝑅‘𝑦))(𝑐‘𝑦))) = (𝑦 ∈ 𝐼 ↦ ((𝑎‘𝑦)(+g‘(𝑅‘𝑦))((𝑏(+g‘𝑌)𝑐)‘𝑦)))) |
44 | 8 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑌) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) → 𝑆 ∈ V) |
45 | 12 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑌) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) → 𝐼 ∈ V) |
46 | 25 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑌) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) → 𝑅 Fn 𝐼) |
47 | 18 | 3adantr3 1222 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑌) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) → (𝑎(+g‘𝑌)𝑏) ∈ (Base‘𝑌)) |
48 | | simpr3 1069 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑌) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) → 𝑐 ∈ (Base‘𝑌)) |
49 | 3, 4, 44, 45, 46, 47, 48, 5 | prdsplusgval 16133 |
. . 3
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑌) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) → ((𝑎(+g‘𝑌)𝑏)(+g‘𝑌)𝑐) = (𝑦 ∈ 𝐼 ↦ (((𝑎(+g‘𝑌)𝑏)‘𝑦)(+g‘(𝑅‘𝑦))(𝑐‘𝑦)))) |
50 | | simpr1 1067 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑌) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) → 𝑎 ∈ (Base‘𝑌)) |
51 | 14 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑌) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) → 𝑅:𝐼⟶Mnd) |
52 | | simpr2 1068 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑌) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) → 𝑏 ∈ (Base‘𝑌)) |
53 | 3, 4, 5, 44, 45, 51, 52, 48 | prdsplusgcl 17321 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑌) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) → (𝑏(+g‘𝑌)𝑐) ∈ (Base‘𝑌)) |
54 | 3, 4, 44, 45, 46, 50, 53, 5 | prdsplusgval 16133 |
. . 3
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑌) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) → (𝑎(+g‘𝑌)(𝑏(+g‘𝑌)𝑐)) = (𝑦 ∈ 𝐼 ↦ ((𝑎‘𝑦)(+g‘(𝑅‘𝑦))((𝑏(+g‘𝑌)𝑐)‘𝑦)))) |
55 | 43, 49, 54 | 3eqtr4d 2666 |
. 2
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑌) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) → ((𝑎(+g‘𝑌)𝑏)(+g‘𝑌)𝑐) = (𝑎(+g‘𝑌)(𝑏(+g‘𝑌)𝑐))) |
56 | | eqid 2622 |
. . . 4
⊢
(0g ∘ 𝑅) = (0g ∘ 𝑅) |
57 | 3, 4, 5, 8, 12, 14, 56 | prdsidlem 17322 |
. . 3
⊢ (𝜑 → ((0g ∘
𝑅) ∈ (Base‘𝑌) ∧ ∀𝑎 ∈ (Base‘𝑌)(((0g ∘ 𝑅)(+g‘𝑌)𝑎) = 𝑎 ∧ (𝑎(+g‘𝑌)(0g ∘ 𝑅)) = 𝑎))) |
58 | 57 | simpld 475 |
. 2
⊢ (𝜑 → (0g ∘
𝑅) ∈ (Base‘𝑌)) |
59 | 57 | simprd 479 |
. . . 4
⊢ (𝜑 → ∀𝑎 ∈ (Base‘𝑌)(((0g ∘ 𝑅)(+g‘𝑌)𝑎) = 𝑎 ∧ (𝑎(+g‘𝑌)(0g ∘ 𝑅)) = 𝑎)) |
60 | 59 | r19.21bi 2932 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ (Base‘𝑌)) → (((0g ∘ 𝑅)(+g‘𝑌)𝑎) = 𝑎 ∧ (𝑎(+g‘𝑌)(0g ∘ 𝑅)) = 𝑎)) |
61 | 60 | simpld 475 |
. 2
⊢ ((𝜑 ∧ 𝑎 ∈ (Base‘𝑌)) → ((0g ∘ 𝑅)(+g‘𝑌)𝑎) = 𝑎) |
62 | 60 | simprd 479 |
. 2
⊢ ((𝜑 ∧ 𝑎 ∈ (Base‘𝑌)) → (𝑎(+g‘𝑌)(0g ∘ 𝑅)) = 𝑎) |
63 | 1, 2, 19, 55, 58, 61, 62 | ismndd 17313 |
1
⊢ (𝜑 → 𝑌 ∈ Mnd) |