Step | Hyp | Ref
| Expression |
1 | | eqidd 2611 |
. 2
⊢ (𝜑 → (Base‘𝑌) = (Base‘𝑌)) |
2 | | eqidd 2611 |
. 2
⊢ (𝜑 → (+g‘𝑌) = (+g‘𝑌)) |
3 | | prdslmodd.y |
. . 3
⊢ 𝑌 = (𝑆Xs𝑅) |
4 | | prdslmodd.s |
. . 3
⊢ (𝜑 → 𝑆 ∈ Ring) |
5 | | prdslmodd.rm |
. . . 4
⊢ (𝜑 → 𝑅:𝐼⟶LMod) |
6 | | prdslmodd.i |
. . . 4
⊢ (𝜑 → 𝐼 ∈ 𝑉) |
7 | | fex 6394 |
. . . 4
⊢ ((𝑅:𝐼⟶LMod ∧ 𝐼 ∈ 𝑉) → 𝑅 ∈ V) |
8 | 5, 6, 7 | syl2anc 691 |
. . 3
⊢ (𝜑 → 𝑅 ∈ V) |
9 | 3, 4, 8 | prdssca 15939 |
. 2
⊢ (𝜑 → 𝑆 = (Scalar‘𝑌)) |
10 | | eqidd 2611 |
. 2
⊢ (𝜑 → (
·𝑠 ‘𝑌) = ( ·𝑠
‘𝑌)) |
11 | | eqidd 2611 |
. 2
⊢ (𝜑 → (Base‘𝑆) = (Base‘𝑆)) |
12 | | eqidd 2611 |
. 2
⊢ (𝜑 → (+g‘𝑆) = (+g‘𝑆)) |
13 | | eqidd 2611 |
. 2
⊢ (𝜑 → (.r‘𝑆) = (.r‘𝑆)) |
14 | | eqidd 2611 |
. 2
⊢ (𝜑 → (1r‘𝑆) = (1r‘𝑆)) |
15 | | lmodgrp 18693 |
. . . . 5
⊢ (𝑎 ∈ LMod → 𝑎 ∈ Grp) |
16 | 15 | ssriv 3572 |
. . . 4
⊢ LMod
⊆ Grp |
17 | | fss 5969 |
. . . 4
⊢ ((𝑅:𝐼⟶LMod ∧ LMod ⊆ Grp) →
𝑅:𝐼⟶Grp) |
18 | 5, 16, 17 | sylancl 693 |
. . 3
⊢ (𝜑 → 𝑅:𝐼⟶Grp) |
19 | 3, 6, 4, 18 | prdsgrpd 17348 |
. 2
⊢ (𝜑 → 𝑌 ∈ Grp) |
20 | | eqid 2610 |
. . . 4
⊢
(Base‘𝑌) =
(Base‘𝑌) |
21 | | eqid 2610 |
. . . 4
⊢ (
·𝑠 ‘𝑌) = ( ·𝑠
‘𝑌) |
22 | | eqid 2610 |
. . . 4
⊢
(Base‘𝑆) =
(Base‘𝑆) |
23 | 4 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑌))) → 𝑆 ∈ Ring) |
24 | | elex 3185 |
. . . . . 6
⊢ (𝐼 ∈ 𝑉 → 𝐼 ∈ V) |
25 | 6, 24 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝐼 ∈ V) |
26 | 25 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑌))) → 𝐼 ∈ V) |
27 | 5 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑌))) → 𝑅:𝐼⟶LMod) |
28 | | simprl 790 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑌))) → 𝑎 ∈ (Base‘𝑆)) |
29 | | simprr 792 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑌))) → 𝑏 ∈ (Base‘𝑌)) |
30 | | prdslmodd.rs |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → (Scalar‘(𝑅‘𝑦)) = 𝑆) |
31 | 30 | adantlr 747 |
. . . 4
⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → (Scalar‘(𝑅‘𝑦)) = 𝑆) |
32 | 3, 20, 21, 22, 23, 26, 27, 28, 29, 31 | prdsvscacl 18789 |
. . 3
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑌))) → (𝑎( ·𝑠
‘𝑌)𝑏) ∈ (Base‘𝑌)) |
33 | 32 | 3impb 1252 |
. 2
⊢ ((𝜑 ∧ 𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑌)) → (𝑎( ·𝑠
‘𝑌)𝑏) ∈ (Base‘𝑌)) |
34 | 5 | ffvelrnda 6267 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → (𝑅‘𝑦) ∈ LMod) |
35 | 34 | adantlr 747 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → (𝑅‘𝑦) ∈ LMod) |
36 | | simplr1 1096 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → 𝑎 ∈ (Base‘𝑆)) |
37 | 30 | fveq2d 6107 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → (Base‘(Scalar‘(𝑅‘𝑦))) = (Base‘𝑆)) |
38 | 37 | adantlr 747 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → (Base‘(Scalar‘(𝑅‘𝑦))) = (Base‘𝑆)) |
39 | 36, 38 | eleqtrrd 2691 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → 𝑎 ∈ (Base‘(Scalar‘(𝑅‘𝑦)))) |
40 | 4 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → 𝑆 ∈ Ring) |
41 | 25 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → 𝐼 ∈ V) |
42 | | ffn 5958 |
. . . . . . . . 9
⊢ (𝑅:𝐼⟶LMod → 𝑅 Fn 𝐼) |
43 | 5, 42 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑅 Fn 𝐼) |
44 | 43 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → 𝑅 Fn 𝐼) |
45 | | simplr2 1097 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → 𝑏 ∈ (Base‘𝑌)) |
46 | | simpr 476 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → 𝑦 ∈ 𝐼) |
47 | 3, 20, 40, 41, 44, 45, 46 | prdsbasprj 15955 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → (𝑏‘𝑦) ∈ (Base‘(𝑅‘𝑦))) |
48 | | simplr3 1098 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → 𝑐 ∈ (Base‘𝑌)) |
49 | 3, 20, 40, 41, 44, 48, 46 | prdsbasprj 15955 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → (𝑐‘𝑦) ∈ (Base‘(𝑅‘𝑦))) |
50 | | eqid 2610 |
. . . . . . 7
⊢
(Base‘(𝑅‘𝑦)) = (Base‘(𝑅‘𝑦)) |
51 | | eqid 2610 |
. . . . . . 7
⊢
(+g‘(𝑅‘𝑦)) = (+g‘(𝑅‘𝑦)) |
52 | | eqid 2610 |
. . . . . . 7
⊢
(Scalar‘(𝑅‘𝑦)) = (Scalar‘(𝑅‘𝑦)) |
53 | | eqid 2610 |
. . . . . . 7
⊢ (
·𝑠 ‘(𝑅‘𝑦)) = ( ·𝑠
‘(𝑅‘𝑦)) |
54 | | eqid 2610 |
. . . . . . 7
⊢
(Base‘(Scalar‘(𝑅‘𝑦))) = (Base‘(Scalar‘(𝑅‘𝑦))) |
55 | 50, 51, 52, 53, 54 | lmodvsdi 18709 |
. . . . . 6
⊢ (((𝑅‘𝑦) ∈ LMod ∧ (𝑎 ∈ (Base‘(Scalar‘(𝑅‘𝑦))) ∧ (𝑏‘𝑦) ∈ (Base‘(𝑅‘𝑦)) ∧ (𝑐‘𝑦) ∈ (Base‘(𝑅‘𝑦)))) → (𝑎( ·𝑠
‘(𝑅‘𝑦))((𝑏‘𝑦)(+g‘(𝑅‘𝑦))(𝑐‘𝑦))) = ((𝑎( ·𝑠
‘(𝑅‘𝑦))(𝑏‘𝑦))(+g‘(𝑅‘𝑦))(𝑎( ·𝑠
‘(𝑅‘𝑦))(𝑐‘𝑦)))) |
56 | 35, 39, 47, 49, 55 | syl13anc 1320 |
. . . . 5
⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → (𝑎( ·𝑠
‘(𝑅‘𝑦))((𝑏‘𝑦)(+g‘(𝑅‘𝑦))(𝑐‘𝑦))) = ((𝑎( ·𝑠
‘(𝑅‘𝑦))(𝑏‘𝑦))(+g‘(𝑅‘𝑦))(𝑎( ·𝑠
‘(𝑅‘𝑦))(𝑐‘𝑦)))) |
57 | | eqid 2610 |
. . . . . . 7
⊢
(+g‘𝑌) = (+g‘𝑌) |
58 | 3, 20, 40, 41, 44, 45, 48, 57, 46 | prdsplusgfval 15957 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → ((𝑏(+g‘𝑌)𝑐)‘𝑦) = ((𝑏‘𝑦)(+g‘(𝑅‘𝑦))(𝑐‘𝑦))) |
59 | 58 | oveq2d 6565 |
. . . . 5
⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → (𝑎( ·𝑠
‘(𝑅‘𝑦))((𝑏(+g‘𝑌)𝑐)‘𝑦)) = (𝑎( ·𝑠
‘(𝑅‘𝑦))((𝑏‘𝑦)(+g‘(𝑅‘𝑦))(𝑐‘𝑦)))) |
60 | 3, 20, 21, 22, 40, 41, 44, 36, 45, 46 | prdsvscafval 15963 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → ((𝑎( ·𝑠
‘𝑌)𝑏)‘𝑦) = (𝑎( ·𝑠
‘(𝑅‘𝑦))(𝑏‘𝑦))) |
61 | 3, 20, 21, 22, 40, 41, 44, 36, 48, 46 | prdsvscafval 15963 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → ((𝑎( ·𝑠
‘𝑌)𝑐)‘𝑦) = (𝑎( ·𝑠
‘(𝑅‘𝑦))(𝑐‘𝑦))) |
62 | 60, 61 | oveq12d 6567 |
. . . . 5
⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → (((𝑎( ·𝑠
‘𝑌)𝑏)‘𝑦)(+g‘(𝑅‘𝑦))((𝑎( ·𝑠
‘𝑌)𝑐)‘𝑦)) = ((𝑎( ·𝑠
‘(𝑅‘𝑦))(𝑏‘𝑦))(+g‘(𝑅‘𝑦))(𝑎( ·𝑠
‘(𝑅‘𝑦))(𝑐‘𝑦)))) |
63 | 56, 59, 62 | 3eqtr4d 2654 |
. . . 4
⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → (𝑎( ·𝑠
‘(𝑅‘𝑦))((𝑏(+g‘𝑌)𝑐)‘𝑦)) = (((𝑎( ·𝑠
‘𝑌)𝑏)‘𝑦)(+g‘(𝑅‘𝑦))((𝑎( ·𝑠
‘𝑌)𝑐)‘𝑦))) |
64 | 63 | mpteq2dva 4672 |
. . 3
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) → (𝑦 ∈ 𝐼 ↦ (𝑎( ·𝑠
‘(𝑅‘𝑦))((𝑏(+g‘𝑌)𝑐)‘𝑦))) = (𝑦 ∈ 𝐼 ↦ (((𝑎( ·𝑠
‘𝑌)𝑏)‘𝑦)(+g‘(𝑅‘𝑦))((𝑎( ·𝑠
‘𝑌)𝑐)‘𝑦)))) |
65 | 4 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) → 𝑆 ∈ Ring) |
66 | 25 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) → 𝐼 ∈ V) |
67 | 43 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) → 𝑅 Fn 𝐼) |
68 | | simpr1 1060 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) → 𝑎 ∈ (Base‘𝑆)) |
69 | 19 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) → 𝑌 ∈ Grp) |
70 | | simpr2 1061 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) → 𝑏 ∈ (Base‘𝑌)) |
71 | | simpr3 1062 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) → 𝑐 ∈ (Base‘𝑌)) |
72 | 20, 57 | grpcl 17253 |
. . . . 5
⊢ ((𝑌 ∈ Grp ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌)) → (𝑏(+g‘𝑌)𝑐) ∈ (Base‘𝑌)) |
73 | 69, 70, 71, 72 | syl3anc 1318 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) → (𝑏(+g‘𝑌)𝑐) ∈ (Base‘𝑌)) |
74 | 3, 20, 21, 22, 65, 66, 67, 68, 73 | prdsvscaval 15962 |
. . 3
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) → (𝑎( ·𝑠
‘𝑌)(𝑏(+g‘𝑌)𝑐)) = (𝑦 ∈ 𝐼 ↦ (𝑎( ·𝑠
‘(𝑅‘𝑦))((𝑏(+g‘𝑌)𝑐)‘𝑦)))) |
75 | 32 | 3adantr3 1215 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) → (𝑎( ·𝑠
‘𝑌)𝑏) ∈ (Base‘𝑌)) |
76 | 4 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑐 ∈ (Base‘𝑌))) → 𝑆 ∈ Ring) |
77 | 25 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑐 ∈ (Base‘𝑌))) → 𝐼 ∈ V) |
78 | 5 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑐 ∈ (Base‘𝑌))) → 𝑅:𝐼⟶LMod) |
79 | | simprl 790 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑐 ∈ (Base‘𝑌))) → 𝑎 ∈ (Base‘𝑆)) |
80 | | simprr 792 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑐 ∈ (Base‘𝑌))) → 𝑐 ∈ (Base‘𝑌)) |
81 | 30 | adantlr 747 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → (Scalar‘(𝑅‘𝑦)) = 𝑆) |
82 | 3, 20, 21, 22, 76, 77, 78, 79, 80, 81 | prdsvscacl 18789 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑐 ∈ (Base‘𝑌))) → (𝑎( ·𝑠
‘𝑌)𝑐) ∈ (Base‘𝑌)) |
83 | 82 | 3adantr2 1214 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) → (𝑎( ·𝑠
‘𝑌)𝑐) ∈ (Base‘𝑌)) |
84 | 3, 20, 65, 66, 67, 75, 83, 57 | prdsplusgval 15956 |
. . 3
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) → ((𝑎( ·𝑠
‘𝑌)𝑏)(+g‘𝑌)(𝑎( ·𝑠
‘𝑌)𝑐)) = (𝑦 ∈ 𝐼 ↦ (((𝑎( ·𝑠
‘𝑌)𝑏)‘𝑦)(+g‘(𝑅‘𝑦))((𝑎( ·𝑠
‘𝑌)𝑐)‘𝑦)))) |
85 | 64, 74, 84 | 3eqtr4d 2654 |
. 2
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑌) ∧ 𝑐 ∈ (Base‘𝑌))) → (𝑎( ·𝑠
‘𝑌)(𝑏(+g‘𝑌)𝑐)) = ((𝑎( ·𝑠
‘𝑌)𝑏)(+g‘𝑌)(𝑎( ·𝑠
‘𝑌)𝑐))) |
86 | 4 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑆) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → 𝑆 ∈ Ring) |
87 | 25 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑆) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → 𝐼 ∈ V) |
88 | 43 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑆) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → 𝑅 Fn 𝐼) |
89 | | simplr1 1096 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑆) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → 𝑎 ∈ (Base‘𝑆)) |
90 | | simplr3 1098 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑆) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → 𝑐 ∈ (Base‘𝑌)) |
91 | | simpr 476 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑆) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → 𝑦 ∈ 𝐼) |
92 | 3, 20, 21, 22, 86, 87, 88, 89, 90, 91 | prdsvscafval 15963 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑆) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → ((𝑎( ·𝑠
‘𝑌)𝑐)‘𝑦) = (𝑎( ·𝑠
‘(𝑅‘𝑦))(𝑐‘𝑦))) |
93 | | simplr2 1097 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑆) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → 𝑏 ∈ (Base‘𝑆)) |
94 | 3, 20, 21, 22, 86, 87, 88, 93, 90, 91 | prdsvscafval 15963 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑆) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → ((𝑏( ·𝑠
‘𝑌)𝑐)‘𝑦) = (𝑏( ·𝑠
‘(𝑅‘𝑦))(𝑐‘𝑦))) |
95 | 92, 94 | oveq12d 6567 |
. . . . 5
⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑆) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → (((𝑎( ·𝑠
‘𝑌)𝑐)‘𝑦)(+g‘(𝑅‘𝑦))((𝑏( ·𝑠
‘𝑌)𝑐)‘𝑦)) = ((𝑎( ·𝑠
‘(𝑅‘𝑦))(𝑐‘𝑦))(+g‘(𝑅‘𝑦))(𝑏( ·𝑠
‘(𝑅‘𝑦))(𝑐‘𝑦)))) |
96 | 34 | adantlr 747 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑆) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → (𝑅‘𝑦) ∈ LMod) |
97 | 37 | adantlr 747 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑆) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → (Base‘(Scalar‘(𝑅‘𝑦))) = (Base‘𝑆)) |
98 | 89, 97 | eleqtrrd 2691 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑆) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → 𝑎 ∈ (Base‘(Scalar‘(𝑅‘𝑦)))) |
99 | 93, 97 | eleqtrrd 2691 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑆) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → 𝑏 ∈ (Base‘(Scalar‘(𝑅‘𝑦)))) |
100 | 3, 20, 86, 87, 88, 90, 91 | prdsbasprj 15955 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑆) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → (𝑐‘𝑦) ∈ (Base‘(𝑅‘𝑦))) |
101 | | eqid 2610 |
. . . . . . 7
⊢
(+g‘(Scalar‘(𝑅‘𝑦))) =
(+g‘(Scalar‘(𝑅‘𝑦))) |
102 | 50, 51, 52, 53, 54, 101 | lmodvsdir 18710 |
. . . . . 6
⊢ (((𝑅‘𝑦) ∈ LMod ∧ (𝑎 ∈ (Base‘(Scalar‘(𝑅‘𝑦))) ∧ 𝑏 ∈ (Base‘(Scalar‘(𝑅‘𝑦))) ∧ (𝑐‘𝑦) ∈ (Base‘(𝑅‘𝑦)))) → ((𝑎(+g‘(Scalar‘(𝑅‘𝑦)))𝑏)( ·𝑠
‘(𝑅‘𝑦))(𝑐‘𝑦)) = ((𝑎( ·𝑠
‘(𝑅‘𝑦))(𝑐‘𝑦))(+g‘(𝑅‘𝑦))(𝑏( ·𝑠
‘(𝑅‘𝑦))(𝑐‘𝑦)))) |
103 | 96, 98, 99, 100, 102 | syl13anc 1320 |
. . . . 5
⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑆) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → ((𝑎(+g‘(Scalar‘(𝑅‘𝑦)))𝑏)( ·𝑠
‘(𝑅‘𝑦))(𝑐‘𝑦)) = ((𝑎( ·𝑠
‘(𝑅‘𝑦))(𝑐‘𝑦))(+g‘(𝑅‘𝑦))(𝑏( ·𝑠
‘(𝑅‘𝑦))(𝑐‘𝑦)))) |
104 | 30 | adantlr 747 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑆) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → (Scalar‘(𝑅‘𝑦)) = 𝑆) |
105 | 104 | fveq2d 6107 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑆) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) →
(+g‘(Scalar‘(𝑅‘𝑦))) = (+g‘𝑆)) |
106 | 105 | oveqd 6566 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑆) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → (𝑎(+g‘(Scalar‘(𝑅‘𝑦)))𝑏) = (𝑎(+g‘𝑆)𝑏)) |
107 | 106 | oveq1d 6564 |
. . . . 5
⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑆) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → ((𝑎(+g‘(Scalar‘(𝑅‘𝑦)))𝑏)( ·𝑠
‘(𝑅‘𝑦))(𝑐‘𝑦)) = ((𝑎(+g‘𝑆)𝑏)( ·𝑠
‘(𝑅‘𝑦))(𝑐‘𝑦))) |
108 | 95, 103, 107 | 3eqtr2rd 2651 |
. . . 4
⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑆) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → ((𝑎(+g‘𝑆)𝑏)( ·𝑠
‘(𝑅‘𝑦))(𝑐‘𝑦)) = (((𝑎( ·𝑠
‘𝑌)𝑐)‘𝑦)(+g‘(𝑅‘𝑦))((𝑏( ·𝑠
‘𝑌)𝑐)‘𝑦))) |
109 | 108 | mpteq2dva 4672 |
. . 3
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑆) ∧ 𝑐 ∈ (Base‘𝑌))) → (𝑦 ∈ 𝐼 ↦ ((𝑎(+g‘𝑆)𝑏)( ·𝑠
‘(𝑅‘𝑦))(𝑐‘𝑦))) = (𝑦 ∈ 𝐼 ↦ (((𝑎( ·𝑠
‘𝑌)𝑐)‘𝑦)(+g‘(𝑅‘𝑦))((𝑏( ·𝑠
‘𝑌)𝑐)‘𝑦)))) |
110 | 4 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑆) ∧ 𝑐 ∈ (Base‘𝑌))) → 𝑆 ∈ Ring) |
111 | 25 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑆) ∧ 𝑐 ∈ (Base‘𝑌))) → 𝐼 ∈ V) |
112 | 43 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑆) ∧ 𝑐 ∈ (Base‘𝑌))) → 𝑅 Fn 𝐼) |
113 | | simpr1 1060 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑆) ∧ 𝑐 ∈ (Base‘𝑌))) → 𝑎 ∈ (Base‘𝑆)) |
114 | | simpr2 1061 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑆) ∧ 𝑐 ∈ (Base‘𝑌))) → 𝑏 ∈ (Base‘𝑆)) |
115 | | eqid 2610 |
. . . . . 6
⊢
(+g‘𝑆) = (+g‘𝑆) |
116 | 22, 115 | ringacl 18401 |
. . . . 5
⊢ ((𝑆 ∈ Ring ∧ 𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑆)) → (𝑎(+g‘𝑆)𝑏) ∈ (Base‘𝑆)) |
117 | 110, 113,
114, 116 | syl3anc 1318 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑆) ∧ 𝑐 ∈ (Base‘𝑌))) → (𝑎(+g‘𝑆)𝑏) ∈ (Base‘𝑆)) |
118 | | simpr3 1062 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑆) ∧ 𝑐 ∈ (Base‘𝑌))) → 𝑐 ∈ (Base‘𝑌)) |
119 | 3, 20, 21, 22, 110, 111, 112, 117, 118 | prdsvscaval 15962 |
. . 3
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑆) ∧ 𝑐 ∈ (Base‘𝑌))) → ((𝑎(+g‘𝑆)𝑏)( ·𝑠
‘𝑌)𝑐) = (𝑦 ∈ 𝐼 ↦ ((𝑎(+g‘𝑆)𝑏)( ·𝑠
‘(𝑅‘𝑦))(𝑐‘𝑦)))) |
120 | 82 | 3adantr2 1214 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑆) ∧ 𝑐 ∈ (Base‘𝑌))) → (𝑎( ·𝑠
‘𝑌)𝑐) ∈ (Base‘𝑌)) |
121 | 5 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑆) ∧ 𝑐 ∈ (Base‘𝑌))) → 𝑅:𝐼⟶LMod) |
122 | 3, 20, 21, 22, 110, 111, 121, 114, 118, 104 | prdsvscacl 18789 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑆) ∧ 𝑐 ∈ (Base‘𝑌))) → (𝑏( ·𝑠
‘𝑌)𝑐) ∈ (Base‘𝑌)) |
123 | 3, 20, 110, 111, 112, 120, 122, 57 | prdsplusgval 15956 |
. . 3
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑆) ∧ 𝑐 ∈ (Base‘𝑌))) → ((𝑎( ·𝑠
‘𝑌)𝑐)(+g‘𝑌)(𝑏( ·𝑠
‘𝑌)𝑐)) = (𝑦 ∈ 𝐼 ↦ (((𝑎( ·𝑠
‘𝑌)𝑐)‘𝑦)(+g‘(𝑅‘𝑦))((𝑏( ·𝑠
‘𝑌)𝑐)‘𝑦)))) |
124 | 109, 119,
123 | 3eqtr4d 2654 |
. 2
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑆) ∧ 𝑐 ∈ (Base‘𝑌))) → ((𝑎(+g‘𝑆)𝑏)( ·𝑠
‘𝑌)𝑐) = ((𝑎( ·𝑠
‘𝑌)𝑐)(+g‘𝑌)(𝑏( ·𝑠
‘𝑌)𝑐))) |
125 | 94 | oveq2d 6565 |
. . . . 5
⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑆) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → (𝑎( ·𝑠
‘(𝑅‘𝑦))((𝑏( ·𝑠
‘𝑌)𝑐)‘𝑦)) = (𝑎( ·𝑠
‘(𝑅‘𝑦))(𝑏( ·𝑠
‘(𝑅‘𝑦))(𝑐‘𝑦)))) |
126 | | eqid 2610 |
. . . . . . 7
⊢
(.r‘(Scalar‘(𝑅‘𝑦))) =
(.r‘(Scalar‘(𝑅‘𝑦))) |
127 | 50, 52, 53, 54, 126 | lmodvsass 18711 |
. . . . . 6
⊢ (((𝑅‘𝑦) ∈ LMod ∧ (𝑎 ∈ (Base‘(Scalar‘(𝑅‘𝑦))) ∧ 𝑏 ∈ (Base‘(Scalar‘(𝑅‘𝑦))) ∧ (𝑐‘𝑦) ∈ (Base‘(𝑅‘𝑦)))) → ((𝑎(.r‘(Scalar‘(𝑅‘𝑦)))𝑏)( ·𝑠
‘(𝑅‘𝑦))(𝑐‘𝑦)) = (𝑎( ·𝑠
‘(𝑅‘𝑦))(𝑏( ·𝑠
‘(𝑅‘𝑦))(𝑐‘𝑦)))) |
128 | 96, 98, 99, 100, 127 | syl13anc 1320 |
. . . . 5
⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑆) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → ((𝑎(.r‘(Scalar‘(𝑅‘𝑦)))𝑏)( ·𝑠
‘(𝑅‘𝑦))(𝑐‘𝑦)) = (𝑎( ·𝑠
‘(𝑅‘𝑦))(𝑏( ·𝑠
‘(𝑅‘𝑦))(𝑐‘𝑦)))) |
129 | 104 | fveq2d 6107 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑆) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) →
(.r‘(Scalar‘(𝑅‘𝑦))) = (.r‘𝑆)) |
130 | 129 | oveqd 6566 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑆) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → (𝑎(.r‘(Scalar‘(𝑅‘𝑦)))𝑏) = (𝑎(.r‘𝑆)𝑏)) |
131 | 130 | oveq1d 6564 |
. . . . 5
⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑆) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → ((𝑎(.r‘(Scalar‘(𝑅‘𝑦)))𝑏)( ·𝑠
‘(𝑅‘𝑦))(𝑐‘𝑦)) = ((𝑎(.r‘𝑆)𝑏)( ·𝑠
‘(𝑅‘𝑦))(𝑐‘𝑦))) |
132 | 125, 128,
131 | 3eqtr2rd 2651 |
. . . 4
⊢ (((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑆) ∧ 𝑐 ∈ (Base‘𝑌))) ∧ 𝑦 ∈ 𝐼) → ((𝑎(.r‘𝑆)𝑏)( ·𝑠
‘(𝑅‘𝑦))(𝑐‘𝑦)) = (𝑎( ·𝑠
‘(𝑅‘𝑦))((𝑏( ·𝑠
‘𝑌)𝑐)‘𝑦))) |
133 | 132 | mpteq2dva 4672 |
. . 3
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑆) ∧ 𝑐 ∈ (Base‘𝑌))) → (𝑦 ∈ 𝐼 ↦ ((𝑎(.r‘𝑆)𝑏)( ·𝑠
‘(𝑅‘𝑦))(𝑐‘𝑦))) = (𝑦 ∈ 𝐼 ↦ (𝑎( ·𝑠
‘(𝑅‘𝑦))((𝑏( ·𝑠
‘𝑌)𝑐)‘𝑦)))) |
134 | | eqid 2610 |
. . . . . 6
⊢
(.r‘𝑆) = (.r‘𝑆) |
135 | 22, 134 | ringcl 18384 |
. . . . 5
⊢ ((𝑆 ∈ Ring ∧ 𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑆)) → (𝑎(.r‘𝑆)𝑏) ∈ (Base‘𝑆)) |
136 | 110, 113,
114, 135 | syl3anc 1318 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑆) ∧ 𝑐 ∈ (Base‘𝑌))) → (𝑎(.r‘𝑆)𝑏) ∈ (Base‘𝑆)) |
137 | 3, 20, 21, 22, 110, 111, 112, 136, 118 | prdsvscaval 15962 |
. . 3
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑆) ∧ 𝑐 ∈ (Base‘𝑌))) → ((𝑎(.r‘𝑆)𝑏)( ·𝑠
‘𝑌)𝑐) = (𝑦 ∈ 𝐼 ↦ ((𝑎(.r‘𝑆)𝑏)( ·𝑠
‘(𝑅‘𝑦))(𝑐‘𝑦)))) |
138 | 3, 20, 21, 22, 110, 111, 112, 113, 122 | prdsvscaval 15962 |
. . 3
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑆) ∧ 𝑐 ∈ (Base‘𝑌))) → (𝑎( ·𝑠
‘𝑌)(𝑏(
·𝑠 ‘𝑌)𝑐)) = (𝑦 ∈ 𝐼 ↦ (𝑎( ·𝑠
‘(𝑅‘𝑦))((𝑏( ·𝑠
‘𝑌)𝑐)‘𝑦)))) |
139 | 133, 137,
138 | 3eqtr4d 2654 |
. 2
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑆) ∧ 𝑏 ∈ (Base‘𝑆) ∧ 𝑐 ∈ (Base‘𝑌))) → ((𝑎(.r‘𝑆)𝑏)( ·𝑠
‘𝑌)𝑐) = (𝑎( ·𝑠
‘𝑌)(𝑏(
·𝑠 ‘𝑌)𝑐))) |
140 | 30 | fveq2d 6107 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) →
(1r‘(Scalar‘(𝑅‘𝑦))) = (1r‘𝑆)) |
141 | 140 | adantlr 747 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ (Base‘𝑌)) ∧ 𝑦 ∈ 𝐼) →
(1r‘(Scalar‘(𝑅‘𝑦))) = (1r‘𝑆)) |
142 | 141 | oveq1d 6564 |
. . . . 5
⊢ (((𝜑 ∧ 𝑎 ∈ (Base‘𝑌)) ∧ 𝑦 ∈ 𝐼) →
((1r‘(Scalar‘(𝑅‘𝑦)))( ·𝑠
‘(𝑅‘𝑦))(𝑎‘𝑦)) = ((1r‘𝑆)( ·𝑠
‘(𝑅‘𝑦))(𝑎‘𝑦))) |
143 | 34 | adantlr 747 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ (Base‘𝑌)) ∧ 𝑦 ∈ 𝐼) → (𝑅‘𝑦) ∈ LMod) |
144 | 4 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ (Base‘𝑌)) ∧ 𝑦 ∈ 𝐼) → 𝑆 ∈ Ring) |
145 | 25 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ (Base‘𝑌)) ∧ 𝑦 ∈ 𝐼) → 𝐼 ∈ V) |
146 | 43 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ (Base‘𝑌)) ∧ 𝑦 ∈ 𝐼) → 𝑅 Fn 𝐼) |
147 | | simplr 788 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ (Base‘𝑌)) ∧ 𝑦 ∈ 𝐼) → 𝑎 ∈ (Base‘𝑌)) |
148 | | simpr 476 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ (Base‘𝑌)) ∧ 𝑦 ∈ 𝐼) → 𝑦 ∈ 𝐼) |
149 | 3, 20, 144, 145, 146, 147, 148 | prdsbasprj 15955 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ (Base‘𝑌)) ∧ 𝑦 ∈ 𝐼) → (𝑎‘𝑦) ∈ (Base‘(𝑅‘𝑦))) |
150 | | eqid 2610 |
. . . . . . 7
⊢
(1r‘(Scalar‘(𝑅‘𝑦))) =
(1r‘(Scalar‘(𝑅‘𝑦))) |
151 | 50, 52, 53, 150 | lmodvs1 18714 |
. . . . . 6
⊢ (((𝑅‘𝑦) ∈ LMod ∧ (𝑎‘𝑦) ∈ (Base‘(𝑅‘𝑦))) →
((1r‘(Scalar‘(𝑅‘𝑦)))( ·𝑠
‘(𝑅‘𝑦))(𝑎‘𝑦)) = (𝑎‘𝑦)) |
152 | 143, 149,
151 | syl2anc 691 |
. . . . 5
⊢ (((𝜑 ∧ 𝑎 ∈ (Base‘𝑌)) ∧ 𝑦 ∈ 𝐼) →
((1r‘(Scalar‘(𝑅‘𝑦)))( ·𝑠
‘(𝑅‘𝑦))(𝑎‘𝑦)) = (𝑎‘𝑦)) |
153 | 142, 152 | eqtr3d 2646 |
. . . 4
⊢ (((𝜑 ∧ 𝑎 ∈ (Base‘𝑌)) ∧ 𝑦 ∈ 𝐼) → ((1r‘𝑆)(
·𝑠 ‘(𝑅‘𝑦))(𝑎‘𝑦)) = (𝑎‘𝑦)) |
154 | 153 | mpteq2dva 4672 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ (Base‘𝑌)) → (𝑦 ∈ 𝐼 ↦ ((1r‘𝑆)(
·𝑠 ‘(𝑅‘𝑦))(𝑎‘𝑦))) = (𝑦 ∈ 𝐼 ↦ (𝑎‘𝑦))) |
155 | 4 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ (Base‘𝑌)) → 𝑆 ∈ Ring) |
156 | 25 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ (Base‘𝑌)) → 𝐼 ∈ V) |
157 | 43 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ (Base‘𝑌)) → 𝑅 Fn 𝐼) |
158 | | eqid 2610 |
. . . . . . 7
⊢
(1r‘𝑆) = (1r‘𝑆) |
159 | 22, 158 | ringidcl 18391 |
. . . . . 6
⊢ (𝑆 ∈ Ring →
(1r‘𝑆)
∈ (Base‘𝑆)) |
160 | 4, 159 | syl 17 |
. . . . 5
⊢ (𝜑 → (1r‘𝑆) ∈ (Base‘𝑆)) |
161 | 160 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ (Base‘𝑌)) → (1r‘𝑆) ∈ (Base‘𝑆)) |
162 | | simpr 476 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ (Base‘𝑌)) → 𝑎 ∈ (Base‘𝑌)) |
163 | 3, 20, 21, 22, 155, 156, 157, 161, 162 | prdsvscaval 15962 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ (Base‘𝑌)) → ((1r‘𝑆)(
·𝑠 ‘𝑌)𝑎) = (𝑦 ∈ 𝐼 ↦ ((1r‘𝑆)(
·𝑠 ‘(𝑅‘𝑦))(𝑎‘𝑦)))) |
164 | 3, 20, 155, 156, 157, 162 | prdsbasfn 15954 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ (Base‘𝑌)) → 𝑎 Fn 𝐼) |
165 | | dffn5 6151 |
. . . 4
⊢ (𝑎 Fn 𝐼 ↔ 𝑎 = (𝑦 ∈ 𝐼 ↦ (𝑎‘𝑦))) |
166 | 164, 165 | sylib 207 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ (Base‘𝑌)) → 𝑎 = (𝑦 ∈ 𝐼 ↦ (𝑎‘𝑦))) |
167 | 154, 163,
166 | 3eqtr4d 2654 |
. 2
⊢ ((𝜑 ∧ 𝑎 ∈ (Base‘𝑌)) → ((1r‘𝑆)(
·𝑠 ‘𝑌)𝑎) = 𝑎) |
168 | 1, 2, 9, 10, 11, 12, 13, 14, 4, 19, 33, 85, 124, 139, 167 | islmodd 18692 |
1
⊢ (𝜑 → 𝑌 ∈ LMod) |