| Step | Hyp | Ref
| Expression |
| 1 | | eqidd 2738 |
. 2
⊢ (𝜑 → (Base‘𝑆) = (Base‘𝑆)) |
| 2 | | eqidd 2738 |
. 2
⊢ (𝜑 → (+g‘𝑆) = (+g‘𝑆)) |
| 3 | | psrring.s |
. . 3
⊢ 𝑆 = (𝐼 mPwSer 𝑅) |
| 4 | | psrring.i |
. . 3
⊢ (𝜑 → 𝐼 ∈ 𝑉) |
| 5 | | psrring.r |
. . 3
⊢ (𝜑 → 𝑅 ∈ Ring) |
| 6 | 3, 4, 5 | psrsca 21967 |
. 2
⊢ (𝜑 → 𝑅 = (Scalar‘𝑆)) |
| 7 | | eqidd 2738 |
. 2
⊢ (𝜑 → (
·𝑠 ‘𝑆) = ( ·𝑠
‘𝑆)) |
| 8 | | eqidd 2738 |
. 2
⊢ (𝜑 → (Base‘𝑅) = (Base‘𝑅)) |
| 9 | | eqidd 2738 |
. 2
⊢ (𝜑 → (+g‘𝑅) = (+g‘𝑅)) |
| 10 | | eqidd 2738 |
. 2
⊢ (𝜑 → (.r‘𝑅) = (.r‘𝑅)) |
| 11 | | eqidd 2738 |
. 2
⊢ (𝜑 → (1r‘𝑅) = (1r‘𝑅)) |
| 12 | | ringgrp 20235 |
. . . 4
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp) |
| 13 | 5, 12 | syl 17 |
. . 3
⊢ (𝜑 → 𝑅 ∈ Grp) |
| 14 | 3, 4, 13 | psrgrp 21976 |
. 2
⊢ (𝜑 → 𝑆 ∈ Grp) |
| 15 | | eqid 2737 |
. . 3
⊢ (
·𝑠 ‘𝑆) = ( ·𝑠
‘𝑆) |
| 16 | | eqid 2737 |
. . 3
⊢
(Base‘𝑅) =
(Base‘𝑅) |
| 17 | | eqid 2737 |
. . 3
⊢
(Base‘𝑆) =
(Base‘𝑆) |
| 18 | 5 | 3ad2ant1 1134 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑆)) → 𝑅 ∈ Ring) |
| 19 | | simp2 1138 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑆)) → 𝑥 ∈ (Base‘𝑅)) |
| 20 | | simp3 1139 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑆)) → 𝑦 ∈ (Base‘𝑆)) |
| 21 | 3, 15, 16, 17, 18, 19, 20 | psrvscacl 21971 |
. 2
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑆)) → (𝑥( ·𝑠
‘𝑆)𝑦) ∈ (Base‘𝑆)) |
| 22 | | ovex 7464 |
. . . . . . 7
⊢
(ℕ0 ↑m 𝐼) ∈ V |
| 23 | 22 | rabex 5339 |
. . . . . 6
⊢ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ∈
V |
| 24 | 23 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (Base‘𝑆))) → {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ∈
V) |
| 25 | | simpr1 1195 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (Base‘𝑆))) → 𝑥 ∈ (Base‘𝑅)) |
| 26 | | fconst6g 6797 |
. . . . . 6
⊢ (𝑥 ∈ (Base‘𝑅) → ({𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} × {𝑥}):{𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈
Fin}⟶(Base‘𝑅)) |
| 27 | 25, 26 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (Base‘𝑆))) → ({𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} × {𝑥}):{𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈
Fin}⟶(Base‘𝑅)) |
| 28 | | eqid 2737 |
. . . . . 6
⊢ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} = {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈
Fin} |
| 29 | | simpr2 1196 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (Base‘𝑆))) → 𝑦 ∈ (Base‘𝑆)) |
| 30 | 3, 16, 28, 17, 29 | psrelbas 21954 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (Base‘𝑆))) → 𝑦:{𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈
Fin}⟶(Base‘𝑅)) |
| 31 | | simpr3 1197 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (Base‘𝑆))) → 𝑧 ∈ (Base‘𝑆)) |
| 32 | 3, 16, 28, 17, 31 | psrelbas 21954 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (Base‘𝑆))) → 𝑧:{𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈
Fin}⟶(Base‘𝑅)) |
| 33 | 5 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (Base‘𝑆))) → 𝑅 ∈ Ring) |
| 34 | | eqid 2737 |
. . . . . . 7
⊢
(+g‘𝑅) = (+g‘𝑅) |
| 35 | | eqid 2737 |
. . . . . . 7
⊢
(.r‘𝑅) = (.r‘𝑅) |
| 36 | 16, 34, 35 | ringdi 20258 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ (𝑟 ∈ (Base‘𝑅) ∧ 𝑠 ∈ (Base‘𝑅) ∧ 𝑡 ∈ (Base‘𝑅))) → (𝑟(.r‘𝑅)(𝑠(+g‘𝑅)𝑡)) = ((𝑟(.r‘𝑅)𝑠)(+g‘𝑅)(𝑟(.r‘𝑅)𝑡))) |
| 37 | 33, 36 | sylan 580 |
. . . . 5
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (Base‘𝑆))) ∧ (𝑟 ∈ (Base‘𝑅) ∧ 𝑠 ∈ (Base‘𝑅) ∧ 𝑡 ∈ (Base‘𝑅))) → (𝑟(.r‘𝑅)(𝑠(+g‘𝑅)𝑡)) = ((𝑟(.r‘𝑅)𝑠)(+g‘𝑅)(𝑟(.r‘𝑅)𝑡))) |
| 38 | 24, 27, 30, 32, 37 | caofdi 7739 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (Base‘𝑆))) → (({𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} × {𝑥}) ∘f
(.r‘𝑅)(𝑦 ∘f
(+g‘𝑅)𝑧)) = ((({𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} × {𝑥}) ∘f
(.r‘𝑅)𝑦) ∘f
(+g‘𝑅)(({𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} × {𝑥}) ∘f
(.r‘𝑅)𝑧))) |
| 39 | | eqid 2737 |
. . . . . 6
⊢
(+g‘𝑆) = (+g‘𝑆) |
| 40 | 3, 17, 34, 39, 29, 31 | psradd 21957 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (Base‘𝑆))) → (𝑦(+g‘𝑆)𝑧) = (𝑦 ∘f
(+g‘𝑅)𝑧)) |
| 41 | 40 | oveq2d 7447 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (Base‘𝑆))) → (({𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} × {𝑥}) ∘f
(.r‘𝑅)(𝑦(+g‘𝑆)𝑧)) = (({𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} × {𝑥}) ∘f
(.r‘𝑅)(𝑦 ∘f
(+g‘𝑅)𝑧))) |
| 42 | 3, 15, 16, 17, 35, 28, 25, 29 | psrvsca 21969 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (Base‘𝑆))) → (𝑥( ·𝑠
‘𝑆)𝑦) = (({𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} × {𝑥}) ∘f
(.r‘𝑅)𝑦)) |
| 43 | 3, 15, 16, 17, 35, 28, 25, 31 | psrvsca 21969 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (Base‘𝑆))) → (𝑥( ·𝑠
‘𝑆)𝑧) = (({𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} × {𝑥}) ∘f
(.r‘𝑅)𝑧)) |
| 44 | 42, 43 | oveq12d 7449 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (Base‘𝑆))) → ((𝑥( ·𝑠
‘𝑆)𝑦) ∘f
(+g‘𝑅)(𝑥( ·𝑠
‘𝑆)𝑧)) = ((({𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} × {𝑥}) ∘f
(.r‘𝑅)𝑦) ∘f
(+g‘𝑅)(({𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} × {𝑥}) ∘f
(.r‘𝑅)𝑧))) |
| 45 | 38, 41, 44 | 3eqtr4d 2787 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (Base‘𝑆))) → (({𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} × {𝑥}) ∘f
(.r‘𝑅)(𝑦(+g‘𝑆)𝑧)) = ((𝑥( ·𝑠
‘𝑆)𝑦) ∘f
(+g‘𝑅)(𝑥( ·𝑠
‘𝑆)𝑧))) |
| 46 | 13 | grpmgmd 18979 |
. . . . . 6
⊢ (𝜑 → 𝑅 ∈ Mgm) |
| 47 | 46 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (Base‘𝑆))) → 𝑅 ∈ Mgm) |
| 48 | 3, 17, 39, 47, 29, 31 | psraddcl 21958 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (Base‘𝑆))) → (𝑦(+g‘𝑆)𝑧) ∈ (Base‘𝑆)) |
| 49 | 3, 15, 16, 17, 35, 28, 25, 48 | psrvsca 21969 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (Base‘𝑆))) → (𝑥( ·𝑠
‘𝑆)(𝑦(+g‘𝑆)𝑧)) = (({𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} × {𝑥}) ∘f
(.r‘𝑅)(𝑦(+g‘𝑆)𝑧))) |
| 50 | 21 | 3adant3r3 1185 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (Base‘𝑆))) → (𝑥( ·𝑠
‘𝑆)𝑦) ∈ (Base‘𝑆)) |
| 51 | 3, 15, 16, 17, 33, 25, 31 | psrvscacl 21971 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (Base‘𝑆))) → (𝑥( ·𝑠
‘𝑆)𝑧) ∈ (Base‘𝑆)) |
| 52 | 3, 17, 34, 39, 50, 51 | psradd 21957 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (Base‘𝑆))) → ((𝑥( ·𝑠
‘𝑆)𝑦)(+g‘𝑆)(𝑥( ·𝑠
‘𝑆)𝑧)) = ((𝑥( ·𝑠
‘𝑆)𝑦) ∘f
(+g‘𝑅)(𝑥( ·𝑠
‘𝑆)𝑧))) |
| 53 | 45, 49, 52 | 3eqtr4d 2787 |
. 2
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (Base‘𝑆))) → (𝑥( ·𝑠
‘𝑆)(𝑦(+g‘𝑆)𝑧)) = ((𝑥( ·𝑠
‘𝑆)𝑦)(+g‘𝑆)(𝑥( ·𝑠
‘𝑆)𝑧))) |
| 54 | | simpr1 1195 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅) ∧ 𝑧 ∈ (Base‘𝑆))) → 𝑥 ∈ (Base‘𝑅)) |
| 55 | | simpr3 1197 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅) ∧ 𝑧 ∈ (Base‘𝑆))) → 𝑧 ∈ (Base‘𝑆)) |
| 56 | 3, 15, 16, 17, 35, 28, 54, 55 | psrvsca 21969 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅) ∧ 𝑧 ∈ (Base‘𝑆))) → (𝑥( ·𝑠
‘𝑆)𝑧) = (({𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} × {𝑥}) ∘f
(.r‘𝑅)𝑧)) |
| 57 | | simpr2 1196 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅) ∧ 𝑧 ∈ (Base‘𝑆))) → 𝑦 ∈ (Base‘𝑅)) |
| 58 | 3, 15, 16, 17, 35, 28, 57, 55 | psrvsca 21969 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅) ∧ 𝑧 ∈ (Base‘𝑆))) → (𝑦( ·𝑠
‘𝑆)𝑧) = (({𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} × {𝑦}) ∘f
(.r‘𝑅)𝑧)) |
| 59 | 56, 58 | oveq12d 7449 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅) ∧ 𝑧 ∈ (Base‘𝑆))) → ((𝑥( ·𝑠
‘𝑆)𝑧) ∘f
(+g‘𝑅)(𝑦( ·𝑠
‘𝑆)𝑧)) = ((({𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} × {𝑥}) ∘f
(.r‘𝑅)𝑧) ∘f
(+g‘𝑅)(({𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} × {𝑦}) ∘f
(.r‘𝑅)𝑧))) |
| 60 | 23 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅) ∧ 𝑧 ∈ (Base‘𝑆))) → {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ∈
V) |
| 61 | 3, 16, 28, 17, 55 | psrelbas 21954 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅) ∧ 𝑧 ∈ (Base‘𝑆))) → 𝑧:{𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈
Fin}⟶(Base‘𝑅)) |
| 62 | 54, 26 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅) ∧ 𝑧 ∈ (Base‘𝑆))) → ({𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} × {𝑥}):{𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈
Fin}⟶(Base‘𝑅)) |
| 63 | | fconst6g 6797 |
. . . . . 6
⊢ (𝑦 ∈ (Base‘𝑅) → ({𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} × {𝑦}):{𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈
Fin}⟶(Base‘𝑅)) |
| 64 | 57, 63 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅) ∧ 𝑧 ∈ (Base‘𝑆))) → ({𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} × {𝑦}):{𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈
Fin}⟶(Base‘𝑅)) |
| 65 | 5 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅) ∧ 𝑧 ∈ (Base‘𝑆))) → 𝑅 ∈ Ring) |
| 66 | 16, 34, 35 | ringdir 20259 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ (𝑟 ∈ (Base‘𝑅) ∧ 𝑠 ∈ (Base‘𝑅) ∧ 𝑡 ∈ (Base‘𝑅))) → ((𝑟(+g‘𝑅)𝑠)(.r‘𝑅)𝑡) = ((𝑟(.r‘𝑅)𝑡)(+g‘𝑅)(𝑠(.r‘𝑅)𝑡))) |
| 67 | 65, 66 | sylan 580 |
. . . . 5
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅) ∧ 𝑧 ∈ (Base‘𝑆))) ∧ (𝑟 ∈ (Base‘𝑅) ∧ 𝑠 ∈ (Base‘𝑅) ∧ 𝑡 ∈ (Base‘𝑅))) → ((𝑟(+g‘𝑅)𝑠)(.r‘𝑅)𝑡) = ((𝑟(.r‘𝑅)𝑡)(+g‘𝑅)(𝑠(.r‘𝑅)𝑡))) |
| 68 | 60, 61, 62, 64, 67 | caofdir 7740 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅) ∧ 𝑧 ∈ (Base‘𝑆))) → ((({𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} × {𝑥}) ∘f
(+g‘𝑅)({𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} × {𝑦})) ∘f
(.r‘𝑅)𝑧) = ((({𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} × {𝑥}) ∘f
(.r‘𝑅)𝑧) ∘f
(+g‘𝑅)(({𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} × {𝑦}) ∘f
(.r‘𝑅)𝑧))) |
| 69 | 60, 54, 57 | ofc12 7727 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅) ∧ 𝑧 ∈ (Base‘𝑆))) → (({𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} × {𝑥}) ∘f
(+g‘𝑅)({𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} × {𝑦})) = ({𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} × {(𝑥(+g‘𝑅)𝑦)})) |
| 70 | 69 | oveq1d 7446 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅) ∧ 𝑧 ∈ (Base‘𝑆))) → ((({𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} × {𝑥}) ∘f
(+g‘𝑅)({𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} × {𝑦})) ∘f
(.r‘𝑅)𝑧) = (({𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} × {(𝑥(+g‘𝑅)𝑦)}) ∘f
(.r‘𝑅)𝑧)) |
| 71 | 59, 68, 70 | 3eqtr2rd 2784 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅) ∧ 𝑧 ∈ (Base‘𝑆))) → (({𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} × {(𝑥(+g‘𝑅)𝑦)}) ∘f
(.r‘𝑅)𝑧) = ((𝑥( ·𝑠
‘𝑆)𝑧) ∘f
(+g‘𝑅)(𝑦( ·𝑠
‘𝑆)𝑧))) |
| 72 | 16, 34 | ringacl 20275 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅)) → (𝑥(+g‘𝑅)𝑦) ∈ (Base‘𝑅)) |
| 73 | 65, 54, 57, 72 | syl3anc 1373 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅) ∧ 𝑧 ∈ (Base‘𝑆))) → (𝑥(+g‘𝑅)𝑦) ∈ (Base‘𝑅)) |
| 74 | 3, 15, 16, 17, 35, 28, 73, 55 | psrvsca 21969 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅) ∧ 𝑧 ∈ (Base‘𝑆))) → ((𝑥(+g‘𝑅)𝑦)( ·𝑠
‘𝑆)𝑧) = (({𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} × {(𝑥(+g‘𝑅)𝑦)}) ∘f
(.r‘𝑅)𝑧)) |
| 75 | 3, 15, 16, 17, 65, 54, 55 | psrvscacl 21971 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅) ∧ 𝑧 ∈ (Base‘𝑆))) → (𝑥( ·𝑠
‘𝑆)𝑧) ∈ (Base‘𝑆)) |
| 76 | 3, 15, 16, 17, 65, 57, 55 | psrvscacl 21971 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅) ∧ 𝑧 ∈ (Base‘𝑆))) → (𝑦( ·𝑠
‘𝑆)𝑧) ∈ (Base‘𝑆)) |
| 77 | 3, 17, 34, 39, 75, 76 | psradd 21957 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅) ∧ 𝑧 ∈ (Base‘𝑆))) → ((𝑥( ·𝑠
‘𝑆)𝑧)(+g‘𝑆)(𝑦( ·𝑠
‘𝑆)𝑧)) = ((𝑥( ·𝑠
‘𝑆)𝑧) ∘f
(+g‘𝑅)(𝑦( ·𝑠
‘𝑆)𝑧))) |
| 78 | 71, 74, 77 | 3eqtr4d 2787 |
. 2
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅) ∧ 𝑧 ∈ (Base‘𝑆))) → ((𝑥(+g‘𝑅)𝑦)( ·𝑠
‘𝑆)𝑧) = ((𝑥( ·𝑠
‘𝑆)𝑧)(+g‘𝑆)(𝑦( ·𝑠
‘𝑆)𝑧))) |
| 79 | 58 | oveq2d 7447 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅) ∧ 𝑧 ∈ (Base‘𝑆))) → (({𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} × {𝑥}) ∘f
(.r‘𝑅)(𝑦( ·𝑠
‘𝑆)𝑧)) = (({𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} × {𝑥}) ∘f
(.r‘𝑅)(({𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} × {𝑦}) ∘f
(.r‘𝑅)𝑧))) |
| 80 | 16, 35 | ringass 20250 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ (𝑟 ∈ (Base‘𝑅) ∧ 𝑠 ∈ (Base‘𝑅) ∧ 𝑡 ∈ (Base‘𝑅))) → ((𝑟(.r‘𝑅)𝑠)(.r‘𝑅)𝑡) = (𝑟(.r‘𝑅)(𝑠(.r‘𝑅)𝑡))) |
| 81 | 65, 80 | sylan 580 |
. . . . 5
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅) ∧ 𝑧 ∈ (Base‘𝑆))) ∧ (𝑟 ∈ (Base‘𝑅) ∧ 𝑠 ∈ (Base‘𝑅) ∧ 𝑡 ∈ (Base‘𝑅))) → ((𝑟(.r‘𝑅)𝑠)(.r‘𝑅)𝑡) = (𝑟(.r‘𝑅)(𝑠(.r‘𝑅)𝑡))) |
| 82 | 60, 62, 64, 61, 81 | caofass 7737 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅) ∧ 𝑧 ∈ (Base‘𝑆))) → ((({𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} × {𝑥}) ∘f
(.r‘𝑅)({𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} × {𝑦})) ∘f
(.r‘𝑅)𝑧) = (({𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} × {𝑥}) ∘f
(.r‘𝑅)(({𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} × {𝑦}) ∘f
(.r‘𝑅)𝑧))) |
| 83 | 60, 54, 57 | ofc12 7727 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅) ∧ 𝑧 ∈ (Base‘𝑆))) → (({𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} × {𝑥}) ∘f
(.r‘𝑅)({𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} × {𝑦})) = ({𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} × {(𝑥(.r‘𝑅)𝑦)})) |
| 84 | 83 | oveq1d 7446 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅) ∧ 𝑧 ∈ (Base‘𝑆))) → ((({𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} × {𝑥}) ∘f
(.r‘𝑅)({𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} × {𝑦})) ∘f
(.r‘𝑅)𝑧) = (({𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} × {(𝑥(.r‘𝑅)𝑦)}) ∘f
(.r‘𝑅)𝑧)) |
| 85 | 79, 82, 84 | 3eqtr2rd 2784 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅) ∧ 𝑧 ∈ (Base‘𝑆))) → (({𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} × {(𝑥(.r‘𝑅)𝑦)}) ∘f
(.r‘𝑅)𝑧) = (({𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} × {𝑥}) ∘f
(.r‘𝑅)(𝑦( ·𝑠
‘𝑆)𝑧))) |
| 86 | 16, 35 | ringcl 20247 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅)) → (𝑥(.r‘𝑅)𝑦) ∈ (Base‘𝑅)) |
| 87 | 65, 54, 57, 86 | syl3anc 1373 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅) ∧ 𝑧 ∈ (Base‘𝑆))) → (𝑥(.r‘𝑅)𝑦) ∈ (Base‘𝑅)) |
| 88 | 3, 15, 16, 17, 35, 28, 87, 55 | psrvsca 21969 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅) ∧ 𝑧 ∈ (Base‘𝑆))) → ((𝑥(.r‘𝑅)𝑦)( ·𝑠
‘𝑆)𝑧) = (({𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} × {(𝑥(.r‘𝑅)𝑦)}) ∘f
(.r‘𝑅)𝑧)) |
| 89 | 3, 15, 16, 17, 35, 28, 54, 76 | psrvsca 21969 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅) ∧ 𝑧 ∈ (Base‘𝑆))) → (𝑥( ·𝑠
‘𝑆)(𝑦(
·𝑠 ‘𝑆)𝑧)) = (({𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} × {𝑥}) ∘f
(.r‘𝑅)(𝑦( ·𝑠
‘𝑆)𝑧))) |
| 90 | 85, 88, 89 | 3eqtr4d 2787 |
. 2
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅) ∧ 𝑧 ∈ (Base‘𝑆))) → ((𝑥(.r‘𝑅)𝑦)( ·𝑠
‘𝑆)𝑧) = (𝑥( ·𝑠
‘𝑆)(𝑦(
·𝑠 ‘𝑆)𝑧))) |
| 91 | 5 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑆)) → 𝑅 ∈ Ring) |
| 92 | | eqid 2737 |
. . . . . 6
⊢
(1r‘𝑅) = (1r‘𝑅) |
| 93 | 16, 92 | ringidcl 20262 |
. . . . 5
⊢ (𝑅 ∈ Ring →
(1r‘𝑅)
∈ (Base‘𝑅)) |
| 94 | 91, 93 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑆)) → (1r‘𝑅) ∈ (Base‘𝑅)) |
| 95 | | simpr 484 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑆)) → 𝑥 ∈ (Base‘𝑆)) |
| 96 | 3, 15, 16, 17, 35, 28, 94, 95 | psrvsca 21969 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑆)) → ((1r‘𝑅)(
·𝑠 ‘𝑆)𝑥) = (({𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ×
{(1r‘𝑅)})
∘f (.r‘𝑅)𝑥)) |
| 97 | 23 | a1i 11 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑆)) → {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ∈
V) |
| 98 | 3, 16, 28, 17, 95 | psrelbas 21954 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑆)) → 𝑥:{𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈
Fin}⟶(Base‘𝑅)) |
| 99 | 16, 35, 92 | ringlidm 20266 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑟 ∈ (Base‘𝑅)) →
((1r‘𝑅)(.r‘𝑅)𝑟) = 𝑟) |
| 100 | 91, 99 | sylan 580 |
. . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑆)) ∧ 𝑟 ∈ (Base‘𝑅)) → ((1r‘𝑅)(.r‘𝑅)𝑟) = 𝑟) |
| 101 | 97, 98, 94, 100 | caofid0l 7730 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑆)) → (({𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ×
{(1r‘𝑅)})
∘f (.r‘𝑅)𝑥) = 𝑥) |
| 102 | 96, 101 | eqtrd 2777 |
. 2
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑆)) → ((1r‘𝑅)(
·𝑠 ‘𝑆)𝑥) = 𝑥) |
| 103 | 1, 2, 6, 7, 8, 9, 10, 11, 5, 14, 21, 53, 78, 90, 102 | islmodd 20864 |
1
⊢ (𝜑 → 𝑆 ∈ LMod) |