| Step | Hyp | Ref
| Expression |
| 1 | | eqidd 2738 |
. 2
⊢ (𝜑 → (Base‘𝑌) = (Base‘𝑌)) |
| 2 | | eqidd 2738 |
. 2
⊢ (𝜑 → (+g‘𝑌) = (+g‘𝑌)) |
| 3 | | prdslmodd.y |
. . 3
⊢ 𝑌 = (𝑆Xs𝑅) |
| 4 | | prdslmodd.s |
. . 3
⊢ (𝜑 → 𝑆 ∈ Ring) |
| 5 | | prdslmodd.rm |
. . . 4
⊢ (𝜑 → 𝑅:𝐼⟶LMod) |
| 6 | | prdslmodd.i |
. . . 4
⊢ (𝜑 → 𝐼 ∈ 𝑉) |
| 7 | 5, 6 | fexd 7247 |
. . 3
⊢ (𝜑 → 𝑅 ∈ V) |
| 8 | 3, 4, 7 | prdssca 17501 |
. 2
⊢ (𝜑 → 𝑆 = (Scalar‘𝑌)) |
| 9 | | eqidd 2738 |
. 2
⊢ (𝜑 → (
·𝑠 ‘𝑌) = ( ·𝑠
‘𝑌)) |
| 10 | | eqidd 2738 |
. 2
⊢ (𝜑 → (Base‘𝑆) = (Base‘𝑆)) |
| 11 | | eqidd 2738 |
. 2
⊢ (𝜑 → (+g‘𝑆) = (+g‘𝑆)) |
| 12 | | eqidd 2738 |
. 2
⊢ (𝜑 → (.r‘𝑆) = (.r‘𝑆)) |
| 13 | | eqidd 2738 |
. 2
⊢ (𝜑 → (1r‘𝑆) = (1r‘𝑆)) |
| 14 | | lmodgrp 20865 |
. . . . 5
⊢ (𝑎 ∈ LMod → 𝑎 ∈ Grp) |
| 15 | 14 | ssriv 3987 |
. . . 4
⊢ LMod
⊆ Grp |
| 16 | | fss 6752 |
. . . 4
⊢ ((𝑅:𝐼⟶LMod ∧ LMod ⊆ Grp) →
𝑅:𝐼⟶Grp) |
| 17 | 5, 15, 16 | sylancl 586 |
. . 3
⊢ (𝜑 → 𝑅:𝐼⟶Grp) |
| 18 | 3, 6, 4, 17 | prdsgrpd 19068 |
. 2
⊢ (𝜑 → 𝑌 ∈ Grp) |
| 19 | | eqid 2737 |
. . . 4
⊢
(Base‘𝑌) =
(Base‘𝑌) |
| 20 | | eqid 2737 |
. . . 4
⊢ (
·𝑠 ‘𝑌) = ( ·𝑠
‘𝑌) |
| 21 | | eqid 2737 |
. . . 4
⊢
(Base‘𝑆) =
(Base‘𝑆) |
| 22 | 4 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑌))) → 𝑆 ∈ Ring) |
| 23 | 6 | elexd 3504 |
. . . . 5
⊢ (𝜑 → 𝐼 ∈ V) |
| 24 | 23 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑌))) → 𝐼 ∈ V) |
| 25 | 5 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑌))) → 𝑅:𝐼⟶LMod) |
| 26 | | simprl 771 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑌))) → 𝑎 ∈ (Base‘𝑆)) |
| 27 | | simprr 773 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑌))) → 𝑏 ∈ (Base‘𝑌)) |
| 28 | | prdslmodd.rs |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → (Scalar‘(𝑅‘𝑦)) = 𝑆) |
| 29 | 28 | adantlr 715 |
. . . 4
⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → (Scalar‘(𝑅‘𝑦)) = 𝑆) |
| 30 | 3, 19, 20, 21, 22, 24, 25, 26, 27, 29 | prdsvscacl 20966 |
. . 3
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑌))) → (𝑎( ·𝑠
‘𝑌)𝑏) ∈ (Base‘𝑌)) |
| 31 | 30 | 3impb 1115 |
. 2
⊢ ((𝜑 ∧ 𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑌)) → (𝑎( ·𝑠
‘𝑌)𝑏) ∈ (Base‘𝑌)) |
| 32 | 5 | ffvelcdmda 7104 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → (𝑅‘𝑦) ∈ LMod) |
| 33 | 32 | adantlr 715 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → (𝑅‘𝑦) ∈ LMod) |
| 34 | | simplr1 1216 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → 𝑎 ∈ (Base‘𝑆)) |
| 35 | 28 | fveq2d 6910 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → (Base‘(Scalar‘(𝑅‘𝑦))) = (Base‘𝑆)) |
| 36 | 35 | adantlr 715 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → (Base‘(Scalar‘(𝑅‘𝑦))) = (Base‘𝑆)) |
| 37 | 34, 36 | eleqtrrd 2844 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → 𝑎 ∈ (Base‘(Scalar‘(𝑅‘𝑦)))) |
| 38 | 4 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → 𝑆 ∈ Ring) |
| 39 | 23 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → 𝐼 ∈ V) |
| 40 | 5 | ffnd 6737 |
. . . . . . . 8
⊢ (𝜑 → 𝑅 Fn 𝐼) |
| 41 | 40 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → 𝑅 Fn 𝐼) |
| 42 | | simplr2 1217 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → 𝑏 ∈ (Base‘𝑌)) |
| 43 | | simpr 484 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → 𝑦 ∈ 𝐼) |
| 44 | 3, 19, 38, 39, 41, 42, 43 | prdsbasprj 17517 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → (𝑏‘𝑦) ∈ (Base‘(𝑅‘𝑦))) |
| 45 | | simplr3 1218 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → 𝑐 ∈ (Base‘𝑌)) |
| 46 | 3, 19, 38, 39, 41, 45, 43 | prdsbasprj 17517 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → (𝑐‘𝑦) ∈ (Base‘(𝑅‘𝑦))) |
| 47 | | eqid 2737 |
. . . . . . 7
⊢
(Base‘(𝑅‘𝑦)) = (Base‘(𝑅‘𝑦)) |
| 48 | | eqid 2737 |
. . . . . . 7
⊢
(+g‘(𝑅‘𝑦)) = (+g‘(𝑅‘𝑦)) |
| 49 | | eqid 2737 |
. . . . . . 7
⊢
(Scalar‘(𝑅‘𝑦)) = (Scalar‘(𝑅‘𝑦)) |
| 50 | | eqid 2737 |
. . . . . . 7
⊢ (
·𝑠 ‘(𝑅‘𝑦)) = ( ·𝑠
‘(𝑅‘𝑦)) |
| 51 | | eqid 2737 |
. . . . . . 7
⊢
(Base‘(Scalar‘(𝑅‘𝑦))) = (Base‘(Scalar‘(𝑅‘𝑦))) |
| 52 | 47, 48, 49, 50, 51 | lmodvsdi 20883 |
. . . . . 6
⊢ (((𝑅‘𝑦) ∈ LMod ∧ (𝑎 ∈ (Base‘(Scalar‘(𝑅‘𝑦))) ∧ (𝑏‘𝑦) ∈ (Base‘(𝑅‘𝑦)) ∧ (𝑐‘𝑦) ∈ (Base‘(𝑅‘𝑦)))) → (𝑎( ·𝑠
‘(𝑅‘𝑦))((𝑏‘𝑦)(+g‘(𝑅‘𝑦))(𝑐‘𝑦))) = ((𝑎( ·𝑠
‘(𝑅‘𝑦))(𝑏‘𝑦))(+g‘(𝑅‘𝑦))(𝑎( ·𝑠
‘(𝑅‘𝑦))(𝑐‘𝑦)))) |
| 53 | 33, 37, 44, 46, 52 | syl13anc 1374 |
. . . . 5
⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → (𝑎( ·𝑠
‘(𝑅‘𝑦))((𝑏‘𝑦)(+g‘(𝑅‘𝑦))(𝑐‘𝑦))) = ((𝑎( ·𝑠
‘(𝑅‘𝑦))(𝑏‘𝑦))(+g‘(𝑅‘𝑦))(𝑎( ·𝑠
‘(𝑅‘𝑦))(𝑐‘𝑦)))) |
| 54 | | eqid 2737 |
. . . . . . 7
⊢
(+g‘𝑌) = (+g‘𝑌) |
| 55 | 3, 19, 38, 39, 41, 42, 45, 54, 43 | prdsplusgfval 17519 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → ((𝑏(+g‘𝑌)𝑐)‘𝑦) = ((𝑏‘𝑦)(+g‘(𝑅‘𝑦))(𝑐‘𝑦))) |
| 56 | 55 | oveq2d 7447 |
. . . . 5
⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → (𝑎( ·𝑠
‘(𝑅‘𝑦))((𝑏(+g‘𝑌)𝑐)‘𝑦)) = (𝑎( ·𝑠
‘(𝑅‘𝑦))((𝑏‘𝑦)(+g‘(𝑅‘𝑦))(𝑐‘𝑦)))) |
| 57 | 3, 19, 20, 21, 38, 39, 41, 34, 42, 43 | prdsvscafval 17525 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → ((𝑎( ·𝑠
‘𝑌)𝑏)‘𝑦) = (𝑎( ·𝑠
‘(𝑅‘𝑦))(𝑏‘𝑦))) |
| 58 | 3, 19, 20, 21, 38, 39, 41, 34, 45, 43 | prdsvscafval 17525 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → ((𝑎( ·𝑠
‘𝑌)𝑐)‘𝑦) = (𝑎( ·𝑠
‘(𝑅‘𝑦))(𝑐‘𝑦))) |
| 59 | 57, 58 | oveq12d 7449 |
. . . . 5
⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → (((𝑎( ·𝑠
‘𝑌)𝑏)‘𝑦)(+g‘(𝑅‘𝑦))((𝑎( ·𝑠
‘𝑌)𝑐)‘𝑦)) = ((𝑎( ·𝑠
‘(𝑅‘𝑦))(𝑏‘𝑦))(+g‘(𝑅‘𝑦))(𝑎( ·𝑠
‘(𝑅‘𝑦))(𝑐‘𝑦)))) |
| 60 | 53, 56, 59 | 3eqtr4d 2787 |
. . . 4
⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → (𝑎( ·𝑠
‘(𝑅‘𝑦))((𝑏(+g‘𝑌)𝑐)‘𝑦)) = (((𝑎( ·𝑠
‘𝑌)𝑏)‘𝑦)(+g‘(𝑅‘𝑦))((𝑎( ·𝑠
‘𝑌)𝑐)‘𝑦))) |
| 61 | 60 | mpteq2dva 5242 |
. . 3
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) → (𝑦 ∈ 𝐼 ↦ (𝑎( ·𝑠
‘(𝑅‘𝑦))((𝑏(+g‘𝑌)𝑐)‘𝑦))) = (𝑦 ∈ 𝐼 ↦ (((𝑎( ·𝑠
‘𝑌)𝑏)‘𝑦)(+g‘(𝑅‘𝑦))((𝑎( ·𝑠
‘𝑌)𝑐)‘𝑦)))) |
| 62 | 4 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) → 𝑆 ∈ Ring) |
| 63 | 23 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) → 𝐼 ∈ V) |
| 64 | 40 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) → 𝑅 Fn 𝐼) |
| 65 | | simpr1 1195 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) → 𝑎 ∈ (Base‘𝑆)) |
| 66 | 18 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) → 𝑌 ∈ Grp) |
| 67 | | simpr2 1196 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) → 𝑏 ∈ (Base‘𝑌)) |
| 68 | | simpr3 1197 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) → 𝑐 ∈ (Base‘𝑌)) |
| 69 | 19, 54 | grpcl 18959 |
. . . . 5
⊢ ((𝑌 ∈ Grp ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌)) → (𝑏(+g‘𝑌)𝑐) ∈ (Base‘𝑌)) |
| 70 | 66, 67, 68, 69 | syl3anc 1373 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) → (𝑏(+g‘𝑌)𝑐) ∈ (Base‘𝑌)) |
| 71 | 3, 19, 20, 21, 62, 63, 64, 65, 70 | prdsvscaval 17524 |
. . 3
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) → (𝑎( ·𝑠
‘𝑌)(𝑏(+g‘𝑌)𝑐)) = (𝑦 ∈ 𝐼 ↦ (𝑎( ·𝑠
‘(𝑅‘𝑦))((𝑏(+g‘𝑌)𝑐)‘𝑦)))) |
| 72 | 30 | 3adantr3 1172 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) → (𝑎( ·𝑠
‘𝑌)𝑏) ∈ (Base‘𝑌)) |
| 73 | 4 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑐 ∈ (Base‘𝑌))) → 𝑆 ∈ Ring) |
| 74 | 23 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑐 ∈ (Base‘𝑌))) → 𝐼 ∈ V) |
| 75 | 5 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑐 ∈ (Base‘𝑌))) → 𝑅:𝐼⟶LMod) |
| 76 | | simprl 771 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑐 ∈ (Base‘𝑌))) → 𝑎 ∈ (Base‘𝑆)) |
| 77 | | simprr 773 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑐 ∈ (Base‘𝑌))) → 𝑐 ∈ (Base‘𝑌)) |
| 78 | 28 | adantlr 715 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → (Scalar‘(𝑅‘𝑦)) = 𝑆) |
| 79 | 3, 19, 20, 21, 73, 74, 75, 76, 77, 78 | prdsvscacl 20966 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑐 ∈ (Base‘𝑌))) → (𝑎( ·𝑠
‘𝑌)𝑐) ∈ (Base‘𝑌)) |
| 80 | 79 | 3adantr2 1171 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) → (𝑎( ·𝑠
‘𝑌)𝑐) ∈ (Base‘𝑌)) |
| 81 | 3, 19, 62, 63, 64, 72, 80, 54 | prdsplusgval 17518 |
. . 3
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) → ((𝑎( ·𝑠
‘𝑌)𝑏)(+g‘𝑌)(𝑎( ·𝑠
‘𝑌)𝑐)) = (𝑦 ∈ 𝐼 ↦ (((𝑎( ·𝑠
‘𝑌)𝑏)‘𝑦)(+g‘(𝑅‘𝑦))((𝑎( ·𝑠
‘𝑌)𝑐)‘𝑦)))) |
| 82 | 61, 71, 81 | 3eqtr4d 2787 |
. 2
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) → (𝑎( ·𝑠
‘𝑌)(𝑏(+g‘𝑌)𝑐)) = ((𝑎( ·𝑠
‘𝑌)𝑏)(+g‘𝑌)(𝑎( ·𝑠
‘𝑌)𝑐))) |
| 83 | 4 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑆) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → 𝑆 ∈ Ring) |
| 84 | 23 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑆) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → 𝐼 ∈ V) |
| 85 | 40 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑆) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → 𝑅 Fn 𝐼) |
| 86 | | simplr1 1216 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑆) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → 𝑎 ∈ (Base‘𝑆)) |
| 87 | | simplr3 1218 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑆) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → 𝑐 ∈ (Base‘𝑌)) |
| 88 | | simpr 484 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑆) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → 𝑦 ∈ 𝐼) |
| 89 | 3, 19, 20, 21, 83, 84, 85, 86, 87, 88 | prdsvscafval 17525 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑆) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → ((𝑎( ·𝑠
‘𝑌)𝑐)‘𝑦) = (𝑎( ·𝑠
‘(𝑅‘𝑦))(𝑐‘𝑦))) |
| 90 | | simplr2 1217 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑆) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → 𝑏 ∈ (Base‘𝑆)) |
| 91 | 3, 19, 20, 21, 83, 84, 85, 90, 87, 88 | prdsvscafval 17525 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑆) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → ((𝑏( ·𝑠
‘𝑌)𝑐)‘𝑦) = (𝑏( ·𝑠
‘(𝑅‘𝑦))(𝑐‘𝑦))) |
| 92 | 89, 91 | oveq12d 7449 |
. . . . 5
⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑆) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → (((𝑎( ·𝑠
‘𝑌)𝑐)‘𝑦)(+g‘(𝑅‘𝑦))((𝑏( ·𝑠
‘𝑌)𝑐)‘𝑦)) = ((𝑎( ·𝑠
‘(𝑅‘𝑦))(𝑐‘𝑦))(+g‘(𝑅‘𝑦))(𝑏( ·𝑠
‘(𝑅‘𝑦))(𝑐‘𝑦)))) |
| 93 | 32 | adantlr 715 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑆) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → (𝑅‘𝑦) ∈ LMod) |
| 94 | 35 | adantlr 715 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑆) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → (Base‘(Scalar‘(𝑅‘𝑦))) = (Base‘𝑆)) |
| 95 | 86, 94 | eleqtrrd 2844 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑆) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → 𝑎 ∈ (Base‘(Scalar‘(𝑅‘𝑦)))) |
| 96 | 90, 94 | eleqtrrd 2844 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑆) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → 𝑏 ∈ (Base‘(Scalar‘(𝑅‘𝑦)))) |
| 97 | 3, 19, 83, 84, 85, 87, 88 | prdsbasprj 17517 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑆) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → (𝑐‘𝑦) ∈ (Base‘(𝑅‘𝑦))) |
| 98 | | eqid 2737 |
. . . . . . 7
⊢
(+g‘(Scalar‘(𝑅‘𝑦))) =
(+g‘(Scalar‘(𝑅‘𝑦))) |
| 99 | 47, 48, 49, 50, 51, 98 | lmodvsdir 20884 |
. . . . . 6
⊢ (((𝑅‘𝑦) ∈ LMod ∧ (𝑎 ∈ (Base‘(Scalar‘(𝑅‘𝑦))) ∧ 𝑏 ∈ (Base‘(Scalar‘(𝑅‘𝑦))) ∧ (𝑐‘𝑦) ∈ (Base‘(𝑅‘𝑦)))) → ((𝑎(+g‘(Scalar‘(𝑅‘𝑦)))𝑏)( ·𝑠
‘(𝑅‘𝑦))(𝑐‘𝑦)) = ((𝑎( ·𝑠
‘(𝑅‘𝑦))(𝑐‘𝑦))(+g‘(𝑅‘𝑦))(𝑏( ·𝑠
‘(𝑅‘𝑦))(𝑐‘𝑦)))) |
| 100 | 93, 95, 96, 97, 99 | syl13anc 1374 |
. . . . 5
⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑆) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → ((𝑎(+g‘(Scalar‘(𝑅‘𝑦)))𝑏)( ·𝑠
‘(𝑅‘𝑦))(𝑐‘𝑦)) = ((𝑎( ·𝑠
‘(𝑅‘𝑦))(𝑐‘𝑦))(+g‘(𝑅‘𝑦))(𝑏( ·𝑠
‘(𝑅‘𝑦))(𝑐‘𝑦)))) |
| 101 | 28 | adantlr 715 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑆) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → (Scalar‘(𝑅‘𝑦)) = 𝑆) |
| 102 | 101 | fveq2d 6910 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑆) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) →
(+g‘(Scalar‘(𝑅‘𝑦))) = (+g‘𝑆)) |
| 103 | 102 | oveqd 7448 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑆) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → (𝑎(+g‘(Scalar‘(𝑅‘𝑦)))𝑏) = (𝑎(+g‘𝑆)𝑏)) |
| 104 | 103 | oveq1d 7446 |
. . . . 5
⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑆) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → ((𝑎(+g‘(Scalar‘(𝑅‘𝑦)))𝑏)( ·𝑠
‘(𝑅‘𝑦))(𝑐‘𝑦)) = ((𝑎(+g‘𝑆)𝑏)( ·𝑠
‘(𝑅‘𝑦))(𝑐‘𝑦))) |
| 105 | 92, 100, 104 | 3eqtr2rd 2784 |
. . . 4
⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑆) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → ((𝑎(+g‘𝑆)𝑏)( ·𝑠
‘(𝑅‘𝑦))(𝑐‘𝑦)) = (((𝑎( ·𝑠
‘𝑌)𝑐)‘𝑦)(+g‘(𝑅‘𝑦))((𝑏( ·𝑠
‘𝑌)𝑐)‘𝑦))) |
| 106 | 105 | mpteq2dva 5242 |
. . 3
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑆) ∧ 𝑐 ∈ (Base‘𝑌))) → (𝑦 ∈ 𝐼 ↦ ((𝑎(+g‘𝑆)𝑏)( ·𝑠
‘(𝑅‘𝑦))(𝑐‘𝑦))) = (𝑦 ∈ 𝐼 ↦ (((𝑎( ·𝑠
‘𝑌)𝑐)‘𝑦)(+g‘(𝑅‘𝑦))((𝑏( ·𝑠
‘𝑌)𝑐)‘𝑦)))) |
| 107 | 4 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑆) ∧ 𝑐 ∈ (Base‘𝑌))) → 𝑆 ∈ Ring) |
| 108 | 23 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑆) ∧ 𝑐 ∈ (Base‘𝑌))) → 𝐼 ∈ V) |
| 109 | 40 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑆) ∧ 𝑐 ∈ (Base‘𝑌))) → 𝑅 Fn 𝐼) |
| 110 | | simpr1 1195 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑆) ∧ 𝑐 ∈ (Base‘𝑌))) → 𝑎 ∈ (Base‘𝑆)) |
| 111 | | simpr2 1196 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑆) ∧ 𝑐 ∈ (Base‘𝑌))) → 𝑏 ∈ (Base‘𝑆)) |
| 112 | | eqid 2737 |
. . . . . 6
⊢
(+g‘𝑆) = (+g‘𝑆) |
| 113 | 21, 112 | ringacl 20275 |
. . . . 5
⊢ ((𝑆 ∈ Ring ∧ 𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑆)) → (𝑎(+g‘𝑆)𝑏) ∈ (Base‘𝑆)) |
| 114 | 107, 110,
111, 113 | syl3anc 1373 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑆) ∧ 𝑐 ∈ (Base‘𝑌))) → (𝑎(+g‘𝑆)𝑏) ∈ (Base‘𝑆)) |
| 115 | | simpr3 1197 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑆) ∧ 𝑐 ∈ (Base‘𝑌))) → 𝑐 ∈ (Base‘𝑌)) |
| 116 | 3, 19, 20, 21, 107, 108, 109, 114, 115 | prdsvscaval 17524 |
. . 3
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑆) ∧ 𝑐 ∈ (Base‘𝑌))) → ((𝑎(+g‘𝑆)𝑏)( ·𝑠
‘𝑌)𝑐) = (𝑦 ∈ 𝐼 ↦ ((𝑎(+g‘𝑆)𝑏)( ·𝑠
‘(𝑅‘𝑦))(𝑐‘𝑦)))) |
| 117 | 79 | 3adantr2 1171 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑆) ∧ 𝑐 ∈ (Base‘𝑌))) → (𝑎( ·𝑠
‘𝑌)𝑐) ∈ (Base‘𝑌)) |
| 118 | 5 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑆) ∧ 𝑐 ∈ (Base‘𝑌))) → 𝑅:𝐼⟶LMod) |
| 119 | 3, 19, 20, 21, 107, 108, 118, 111, 115, 101 | prdsvscacl 20966 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑆) ∧ 𝑐 ∈ (Base‘𝑌))) → (𝑏( ·𝑠
‘𝑌)𝑐) ∈ (Base‘𝑌)) |
| 120 | 3, 19, 107, 108, 109, 117, 119, 54 | prdsplusgval 17518 |
. . 3
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑆) ∧ 𝑐 ∈ (Base‘𝑌))) → ((𝑎( ·𝑠
‘𝑌)𝑐)(+g‘𝑌)(𝑏( ·𝑠
‘𝑌)𝑐)) = (𝑦 ∈ 𝐼 ↦ (((𝑎( ·𝑠
‘𝑌)𝑐)‘𝑦)(+g‘(𝑅‘𝑦))((𝑏( ·𝑠
‘𝑌)𝑐)‘𝑦)))) |
| 121 | 106, 116,
120 | 3eqtr4d 2787 |
. 2
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑆) ∧ 𝑐 ∈ (Base‘𝑌))) → ((𝑎(+g‘𝑆)𝑏)( ·𝑠
‘𝑌)𝑐) = ((𝑎( ·𝑠
‘𝑌)𝑐)(+g‘𝑌)(𝑏( ·𝑠
‘𝑌)𝑐))) |
| 122 | 91 | oveq2d 7447 |
. . . . 5
⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑆) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → (𝑎( ·𝑠
‘(𝑅‘𝑦))((𝑏( ·𝑠
‘𝑌)𝑐)‘𝑦)) = (𝑎( ·𝑠
‘(𝑅‘𝑦))(𝑏( ·𝑠
‘(𝑅‘𝑦))(𝑐‘𝑦)))) |
| 123 | | eqid 2737 |
. . . . . . 7
⊢
(.r‘(Scalar‘(𝑅‘𝑦))) =
(.r‘(Scalar‘(𝑅‘𝑦))) |
| 124 | 47, 49, 50, 51, 123 | lmodvsass 20885 |
. . . . . 6
⊢ (((𝑅‘𝑦) ∈ LMod ∧ (𝑎 ∈ (Base‘(Scalar‘(𝑅‘𝑦))) ∧ 𝑏 ∈ (Base‘(Scalar‘(𝑅‘𝑦))) ∧ (𝑐‘𝑦) ∈ (Base‘(𝑅‘𝑦)))) → ((𝑎(.r‘(Scalar‘(𝑅‘𝑦)))𝑏)( ·𝑠
‘(𝑅‘𝑦))(𝑐‘𝑦)) = (𝑎( ·𝑠
‘(𝑅‘𝑦))(𝑏( ·𝑠
‘(𝑅‘𝑦))(𝑐‘𝑦)))) |
| 125 | 93, 95, 96, 97, 124 | syl13anc 1374 |
. . . . 5
⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑆) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → ((𝑎(.r‘(Scalar‘(𝑅‘𝑦)))𝑏)( ·𝑠
‘(𝑅‘𝑦))(𝑐‘𝑦)) = (𝑎( ·𝑠
‘(𝑅‘𝑦))(𝑏( ·𝑠
‘(𝑅‘𝑦))(𝑐‘𝑦)))) |
| 126 | 101 | fveq2d 6910 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑆) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) →
(.r‘(Scalar‘(𝑅‘𝑦))) = (.r‘𝑆)) |
| 127 | 126 | oveqd 7448 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑆) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → (𝑎(.r‘(Scalar‘(𝑅‘𝑦)))𝑏) = (𝑎(.r‘𝑆)𝑏)) |
| 128 | 127 | oveq1d 7446 |
. . . . 5
⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑆) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → ((𝑎(.r‘(Scalar‘(𝑅‘𝑦)))𝑏)( ·𝑠
‘(𝑅‘𝑦))(𝑐‘𝑦)) = ((𝑎(.r‘𝑆)𝑏)( ·𝑠
‘(𝑅‘𝑦))(𝑐‘𝑦))) |
| 129 | 122, 125,
128 | 3eqtr2rd 2784 |
. . . 4
⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑆) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → ((𝑎(.r‘𝑆)𝑏)( ·𝑠
‘(𝑅‘𝑦))(𝑐‘𝑦)) = (𝑎( ·𝑠
‘(𝑅‘𝑦))((𝑏( ·𝑠
‘𝑌)𝑐)‘𝑦))) |
| 130 | 129 | mpteq2dva 5242 |
. . 3
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑆) ∧ 𝑐 ∈ (Base‘𝑌))) → (𝑦 ∈ 𝐼 ↦ ((𝑎(.r‘𝑆)𝑏)( ·𝑠
‘(𝑅‘𝑦))(𝑐‘𝑦))) = (𝑦 ∈ 𝐼 ↦ (𝑎( ·𝑠
‘(𝑅‘𝑦))((𝑏( ·𝑠
‘𝑌)𝑐)‘𝑦)))) |
| 131 | | eqid 2737 |
. . . . . 6
⊢
(.r‘𝑆) = (.r‘𝑆) |
| 132 | 21, 131 | ringcl 20247 |
. . . . 5
⊢ ((𝑆 ∈ Ring ∧ 𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑆)) → (𝑎(.r‘𝑆)𝑏) ∈ (Base‘𝑆)) |
| 133 | 107, 110,
111, 132 | syl3anc 1373 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑆) ∧ 𝑐 ∈ (Base‘𝑌))) → (𝑎(.r‘𝑆)𝑏) ∈ (Base‘𝑆)) |
| 134 | 3, 19, 20, 21, 107, 108, 109, 133, 115 | prdsvscaval 17524 |
. . 3
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑆) ∧ 𝑐 ∈ (Base‘𝑌))) → ((𝑎(.r‘𝑆)𝑏)( ·𝑠
‘𝑌)𝑐) = (𝑦 ∈ 𝐼 ↦ ((𝑎(.r‘𝑆)𝑏)( ·𝑠
‘(𝑅‘𝑦))(𝑐‘𝑦)))) |
| 135 | 3, 19, 20, 21, 107, 108, 109, 110, 119 | prdsvscaval 17524 |
. . 3
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑆) ∧ 𝑐 ∈ (Base‘𝑌))) → (𝑎( ·𝑠
‘𝑌)(𝑏(
·𝑠 ‘𝑌)𝑐)) = (𝑦 ∈ 𝐼 ↦ (𝑎( ·𝑠
‘(𝑅‘𝑦))((𝑏( ·𝑠
‘𝑌)𝑐)‘𝑦)))) |
| 136 | 130, 134,
135 | 3eqtr4d 2787 |
. 2
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑆) ∧ 𝑐 ∈ (Base‘𝑌))) → ((𝑎(.r‘𝑆)𝑏)( ·𝑠
‘𝑌)𝑐) = (𝑎( ·𝑠
‘𝑌)(𝑏(
·𝑠 ‘𝑌)𝑐))) |
| 137 | 28 | fveq2d 6910 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) →
(1r‘(Scalar‘(𝑅‘𝑦))) = (1r‘𝑆)) |
| 138 | 137 | adantlr 715 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ (Base‘𝑌)) ∧ 𝑦 ∈ 𝐼) →
(1r‘(Scalar‘(𝑅‘𝑦))) = (1r‘𝑆)) |
| 139 | 138 | oveq1d 7446 |
. . . . 5
⊢ (((𝜑 ∧ 𝑎 ∈ (Base‘𝑌)) ∧ 𝑦 ∈ 𝐼) →
((1r‘(Scalar‘(𝑅‘𝑦)))( ·𝑠
‘(𝑅‘𝑦))(𝑎‘𝑦)) = ((1r‘𝑆)( ·𝑠
‘(𝑅‘𝑦))(𝑎‘𝑦))) |
| 140 | 32 | adantlr 715 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ (Base‘𝑌)) ∧ 𝑦 ∈ 𝐼) → (𝑅‘𝑦) ∈ LMod) |
| 141 | 4 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ (Base‘𝑌)) ∧ 𝑦 ∈ 𝐼) → 𝑆 ∈ Ring) |
| 142 | 23 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ (Base‘𝑌)) ∧ 𝑦 ∈ 𝐼) → 𝐼 ∈ V) |
| 143 | 40 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ (Base‘𝑌)) ∧ 𝑦 ∈ 𝐼) → 𝑅 Fn 𝐼) |
| 144 | | simplr 769 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ (Base‘𝑌)) ∧ 𝑦 ∈ 𝐼) → 𝑎 ∈ (Base‘𝑌)) |
| 145 | | simpr 484 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ (Base‘𝑌)) ∧ 𝑦 ∈ 𝐼) → 𝑦 ∈ 𝐼) |
| 146 | 3, 19, 141, 142, 143, 144, 145 | prdsbasprj 17517 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ (Base‘𝑌)) ∧ 𝑦 ∈ 𝐼) → (𝑎‘𝑦) ∈ (Base‘(𝑅‘𝑦))) |
| 147 | | eqid 2737 |
. . . . . . 7
⊢
(1r‘(Scalar‘(𝑅‘𝑦))) =
(1r‘(Scalar‘(𝑅‘𝑦))) |
| 148 | 47, 49, 50, 147 | lmodvs1 20888 |
. . . . . 6
⊢ (((𝑅‘𝑦) ∈ LMod ∧ (𝑎‘𝑦) ∈ (Base‘(𝑅‘𝑦))) →
((1r‘(Scalar‘(𝑅‘𝑦)))( ·𝑠
‘(𝑅‘𝑦))(𝑎‘𝑦)) = (𝑎‘𝑦)) |
| 149 | 140, 146,
148 | syl2anc 584 |
. . . . 5
⊢ (((𝜑 ∧ 𝑎 ∈ (Base‘𝑌)) ∧ 𝑦 ∈ 𝐼) →
((1r‘(Scalar‘(𝑅‘𝑦)))( ·𝑠
‘(𝑅‘𝑦))(𝑎‘𝑦)) = (𝑎‘𝑦)) |
| 150 | 139, 149 | eqtr3d 2779 |
. . . 4
⊢ (((𝜑 ∧ 𝑎 ∈ (Base‘𝑌)) ∧ 𝑦 ∈ 𝐼) → ((1r‘𝑆)(
·𝑠 ‘(𝑅‘𝑦))(𝑎‘𝑦)) = (𝑎‘𝑦)) |
| 151 | 150 | mpteq2dva 5242 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ (Base‘𝑌)) → (𝑦 ∈ 𝐼 ↦ ((1r‘𝑆)(
·𝑠 ‘(𝑅‘𝑦))(𝑎‘𝑦))) = (𝑦 ∈ 𝐼 ↦ (𝑎‘𝑦))) |
| 152 | 4 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ (Base‘𝑌)) → 𝑆 ∈ Ring) |
| 153 | 23 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ (Base‘𝑌)) → 𝐼 ∈ V) |
| 154 | 40 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ (Base‘𝑌)) → 𝑅 Fn 𝐼) |
| 155 | | eqid 2737 |
. . . . . . 7
⊢
(1r‘𝑆) = (1r‘𝑆) |
| 156 | 21, 155 | ringidcl 20262 |
. . . . . 6
⊢ (𝑆 ∈ Ring →
(1r‘𝑆)
∈ (Base‘𝑆)) |
| 157 | 4, 156 | syl 17 |
. . . . 5
⊢ (𝜑 → (1r‘𝑆) ∈ (Base‘𝑆)) |
| 158 | 157 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ (Base‘𝑌)) → (1r‘𝑆) ∈ (Base‘𝑆)) |
| 159 | | simpr 484 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ (Base‘𝑌)) → 𝑎 ∈ (Base‘𝑌)) |
| 160 | 3, 19, 20, 21, 152, 153, 154, 158, 159 | prdsvscaval 17524 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ (Base‘𝑌)) → ((1r‘𝑆)(
·𝑠 ‘𝑌)𝑎) = (𝑦 ∈ 𝐼 ↦ ((1r‘𝑆)(
·𝑠 ‘(𝑅‘𝑦))(𝑎‘𝑦)))) |
| 161 | 3, 19, 152, 153, 154, 159 | prdsbasfn 17516 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ (Base‘𝑌)) → 𝑎 Fn 𝐼) |
| 162 | | dffn5 6967 |
. . . 4
⊢ (𝑎 Fn 𝐼 ↔ 𝑎 = (𝑦 ∈ 𝐼 ↦ (𝑎‘𝑦))) |
| 163 | 161, 162 | sylib 218 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ (Base‘𝑌)) → 𝑎 = (𝑦 ∈ 𝐼 ↦ (𝑎‘𝑦))) |
| 164 | 151, 160,
163 | 3eqtr4d 2787 |
. 2
⊢ ((𝜑 ∧ 𝑎 ∈ (Base‘𝑌)) → ((1r‘𝑆)(
·𝑠 ‘𝑌)𝑎) = 𝑎) |
| 165 | 1, 2, 8, 9, 10, 11, 12, 13, 4, 18, 31, 82, 121, 136, 164 | islmodd 20864 |
1
⊢ (𝜑 → 𝑌 ∈ LMod) |