Step |
Hyp |
Ref |
Expression |
1 |
|
psrring.s |
⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 ) |
2 |
|
psrring.i |
⊢ ( 𝜑 → 𝐼 ∈ 𝑉 ) |
3 |
|
psrring.r |
⊢ ( 𝜑 → 𝑅 ∈ Ring ) |
4 |
|
eqidd |
⊢ ( 𝜑 → ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 ) ) |
5 |
|
eqidd |
⊢ ( 𝜑 → ( +g ‘ 𝑆 ) = ( +g ‘ 𝑆 ) ) |
6 |
1 2 3
|
psrsca |
⊢ ( 𝜑 → 𝑅 = ( Scalar ‘ 𝑆 ) ) |
7 |
|
eqidd |
⊢ ( 𝜑 → ( ·𝑠 ‘ 𝑆 ) = ( ·𝑠 ‘ 𝑆 ) ) |
8 |
|
eqidd |
⊢ ( 𝜑 → ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 ) ) |
9 |
|
eqidd |
⊢ ( 𝜑 → ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 ) ) |
10 |
|
eqidd |
⊢ ( 𝜑 → ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 ) ) |
11 |
|
eqidd |
⊢ ( 𝜑 → ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 ) ) |
12 |
|
ringgrp |
⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Grp ) |
13 |
3 12
|
syl |
⊢ ( 𝜑 → 𝑅 ∈ Grp ) |
14 |
1 2 13
|
psrgrp |
⊢ ( 𝜑 → 𝑆 ∈ Grp ) |
15 |
|
eqid |
⊢ ( ·𝑠 ‘ 𝑆 ) = ( ·𝑠 ‘ 𝑆 ) |
16 |
|
eqid |
⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 ) |
17 |
|
eqid |
⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 ) |
18 |
3
|
3ad2ant1 |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) → 𝑅 ∈ Ring ) |
19 |
|
simp2 |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) → 𝑥 ∈ ( Base ‘ 𝑅 ) ) |
20 |
|
simp3 |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) → 𝑦 ∈ ( Base ‘ 𝑆 ) ) |
21 |
1 15 16 17 18 19 20
|
psrvscacl |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) → ( 𝑥 ( ·𝑠 ‘ 𝑆 ) 𝑦 ) ∈ ( Base ‘ 𝑆 ) ) |
22 |
|
ovex |
⊢ ( ℕ0 ↑m 𝐼 ) ∈ V |
23 |
22
|
rabex |
⊢ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∈ V |
24 |
23
|
a1i |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) → { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∈ V ) |
25 |
|
simpr1 |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) → 𝑥 ∈ ( Base ‘ 𝑅 ) ) |
26 |
|
fconst6g |
⊢ ( 𝑥 ∈ ( Base ‘ 𝑅 ) → ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } × { 𝑥 } ) : { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝑅 ) ) |
27 |
25 26
|
syl |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) → ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } × { 𝑥 } ) : { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝑅 ) ) |
28 |
|
eqid |
⊢ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } |
29 |
|
simpr2 |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) → 𝑦 ∈ ( Base ‘ 𝑆 ) ) |
30 |
1 16 28 17 29
|
psrelbas |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) → 𝑦 : { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝑅 ) ) |
31 |
|
simpr3 |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) → 𝑧 ∈ ( Base ‘ 𝑆 ) ) |
32 |
1 16 28 17 31
|
psrelbas |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) → 𝑧 : { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝑅 ) ) |
33 |
3
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) → 𝑅 ∈ Ring ) |
34 |
|
eqid |
⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 ) |
35 |
|
eqid |
⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 ) |
36 |
16 34 35
|
ringdi |
⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑟 ∈ ( Base ‘ 𝑅 ) ∧ 𝑠 ∈ ( Base ‘ 𝑅 ) ∧ 𝑡 ∈ ( Base ‘ 𝑅 ) ) ) → ( 𝑟 ( .r ‘ 𝑅 ) ( 𝑠 ( +g ‘ 𝑅 ) 𝑡 ) ) = ( ( 𝑟 ( .r ‘ 𝑅 ) 𝑠 ) ( +g ‘ 𝑅 ) ( 𝑟 ( .r ‘ 𝑅 ) 𝑡 ) ) ) |
37 |
33 36
|
sylan |
⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) ∧ ( 𝑟 ∈ ( Base ‘ 𝑅 ) ∧ 𝑠 ∈ ( Base ‘ 𝑅 ) ∧ 𝑡 ∈ ( Base ‘ 𝑅 ) ) ) → ( 𝑟 ( .r ‘ 𝑅 ) ( 𝑠 ( +g ‘ 𝑅 ) 𝑡 ) ) = ( ( 𝑟 ( .r ‘ 𝑅 ) 𝑠 ) ( +g ‘ 𝑅 ) ( 𝑟 ( .r ‘ 𝑅 ) 𝑡 ) ) ) |
38 |
24 27 30 32 37
|
caofdi |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) → ( ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } × { 𝑥 } ) ∘f ( .r ‘ 𝑅 ) ( 𝑦 ∘f ( +g ‘ 𝑅 ) 𝑧 ) ) = ( ( ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } × { 𝑥 } ) ∘f ( .r ‘ 𝑅 ) 𝑦 ) ∘f ( +g ‘ 𝑅 ) ( ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } × { 𝑥 } ) ∘f ( .r ‘ 𝑅 ) 𝑧 ) ) ) |
39 |
|
eqid |
⊢ ( +g ‘ 𝑆 ) = ( +g ‘ 𝑆 ) |
40 |
1 17 34 39 29 31
|
psradd |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) → ( 𝑦 ( +g ‘ 𝑆 ) 𝑧 ) = ( 𝑦 ∘f ( +g ‘ 𝑅 ) 𝑧 ) ) |
41 |
40
|
oveq2d |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) → ( ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } × { 𝑥 } ) ∘f ( .r ‘ 𝑅 ) ( 𝑦 ( +g ‘ 𝑆 ) 𝑧 ) ) = ( ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } × { 𝑥 } ) ∘f ( .r ‘ 𝑅 ) ( 𝑦 ∘f ( +g ‘ 𝑅 ) 𝑧 ) ) ) |
42 |
1 15 16 17 35 28 25 29
|
psrvsca |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) → ( 𝑥 ( ·𝑠 ‘ 𝑆 ) 𝑦 ) = ( ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } × { 𝑥 } ) ∘f ( .r ‘ 𝑅 ) 𝑦 ) ) |
43 |
1 15 16 17 35 28 25 31
|
psrvsca |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) → ( 𝑥 ( ·𝑠 ‘ 𝑆 ) 𝑧 ) = ( ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } × { 𝑥 } ) ∘f ( .r ‘ 𝑅 ) 𝑧 ) ) |
44 |
42 43
|
oveq12d |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) → ( ( 𝑥 ( ·𝑠 ‘ 𝑆 ) 𝑦 ) ∘f ( +g ‘ 𝑅 ) ( 𝑥 ( ·𝑠 ‘ 𝑆 ) 𝑧 ) ) = ( ( ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } × { 𝑥 } ) ∘f ( .r ‘ 𝑅 ) 𝑦 ) ∘f ( +g ‘ 𝑅 ) ( ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } × { 𝑥 } ) ∘f ( .r ‘ 𝑅 ) 𝑧 ) ) ) |
45 |
38 41 44
|
3eqtr4d |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) → ( ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } × { 𝑥 } ) ∘f ( .r ‘ 𝑅 ) ( 𝑦 ( +g ‘ 𝑆 ) 𝑧 ) ) = ( ( 𝑥 ( ·𝑠 ‘ 𝑆 ) 𝑦 ) ∘f ( +g ‘ 𝑅 ) ( 𝑥 ( ·𝑠 ‘ 𝑆 ) 𝑧 ) ) ) |
46 |
13
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) → 𝑅 ∈ Grp ) |
47 |
1 17 39 46 29 31
|
psraddcl |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) → ( 𝑦 ( +g ‘ 𝑆 ) 𝑧 ) ∈ ( Base ‘ 𝑆 ) ) |
48 |
1 15 16 17 35 28 25 47
|
psrvsca |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) → ( 𝑥 ( ·𝑠 ‘ 𝑆 ) ( 𝑦 ( +g ‘ 𝑆 ) 𝑧 ) ) = ( ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } × { 𝑥 } ) ∘f ( .r ‘ 𝑅 ) ( 𝑦 ( +g ‘ 𝑆 ) 𝑧 ) ) ) |
49 |
21
|
3adant3r3 |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) → ( 𝑥 ( ·𝑠 ‘ 𝑆 ) 𝑦 ) ∈ ( Base ‘ 𝑆 ) ) |
50 |
1 15 16 17 33 25 31
|
psrvscacl |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) → ( 𝑥 ( ·𝑠 ‘ 𝑆 ) 𝑧 ) ∈ ( Base ‘ 𝑆 ) ) |
51 |
1 17 34 39 49 50
|
psradd |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) → ( ( 𝑥 ( ·𝑠 ‘ 𝑆 ) 𝑦 ) ( +g ‘ 𝑆 ) ( 𝑥 ( ·𝑠 ‘ 𝑆 ) 𝑧 ) ) = ( ( 𝑥 ( ·𝑠 ‘ 𝑆 ) 𝑦 ) ∘f ( +g ‘ 𝑅 ) ( 𝑥 ( ·𝑠 ‘ 𝑆 ) 𝑧 ) ) ) |
52 |
45 48 51
|
3eqtr4d |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) → ( 𝑥 ( ·𝑠 ‘ 𝑆 ) ( 𝑦 ( +g ‘ 𝑆 ) 𝑧 ) ) = ( ( 𝑥 ( ·𝑠 ‘ 𝑆 ) 𝑦 ) ( +g ‘ 𝑆 ) ( 𝑥 ( ·𝑠 ‘ 𝑆 ) 𝑧 ) ) ) |
53 |
|
simpr1 |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) → 𝑥 ∈ ( Base ‘ 𝑅 ) ) |
54 |
|
simpr3 |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) → 𝑧 ∈ ( Base ‘ 𝑆 ) ) |
55 |
1 15 16 17 35 28 53 54
|
psrvsca |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) → ( 𝑥 ( ·𝑠 ‘ 𝑆 ) 𝑧 ) = ( ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } × { 𝑥 } ) ∘f ( .r ‘ 𝑅 ) 𝑧 ) ) |
56 |
|
simpr2 |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) → 𝑦 ∈ ( Base ‘ 𝑅 ) ) |
57 |
1 15 16 17 35 28 56 54
|
psrvsca |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) → ( 𝑦 ( ·𝑠 ‘ 𝑆 ) 𝑧 ) = ( ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } × { 𝑦 } ) ∘f ( .r ‘ 𝑅 ) 𝑧 ) ) |
58 |
55 57
|
oveq12d |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) → ( ( 𝑥 ( ·𝑠 ‘ 𝑆 ) 𝑧 ) ∘f ( +g ‘ 𝑅 ) ( 𝑦 ( ·𝑠 ‘ 𝑆 ) 𝑧 ) ) = ( ( ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } × { 𝑥 } ) ∘f ( .r ‘ 𝑅 ) 𝑧 ) ∘f ( +g ‘ 𝑅 ) ( ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } × { 𝑦 } ) ∘f ( .r ‘ 𝑅 ) 𝑧 ) ) ) |
59 |
23
|
a1i |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) → { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∈ V ) |
60 |
1 16 28 17 54
|
psrelbas |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) → 𝑧 : { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝑅 ) ) |
61 |
53 26
|
syl |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) → ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } × { 𝑥 } ) : { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝑅 ) ) |
62 |
|
fconst6g |
⊢ ( 𝑦 ∈ ( Base ‘ 𝑅 ) → ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } × { 𝑦 } ) : { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝑅 ) ) |
63 |
56 62
|
syl |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) → ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } × { 𝑦 } ) : { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝑅 ) ) |
64 |
3
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) → 𝑅 ∈ Ring ) |
65 |
16 34 35
|
ringdir |
⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑟 ∈ ( Base ‘ 𝑅 ) ∧ 𝑠 ∈ ( Base ‘ 𝑅 ) ∧ 𝑡 ∈ ( Base ‘ 𝑅 ) ) ) → ( ( 𝑟 ( +g ‘ 𝑅 ) 𝑠 ) ( .r ‘ 𝑅 ) 𝑡 ) = ( ( 𝑟 ( .r ‘ 𝑅 ) 𝑡 ) ( +g ‘ 𝑅 ) ( 𝑠 ( .r ‘ 𝑅 ) 𝑡 ) ) ) |
66 |
64 65
|
sylan |
⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) ∧ ( 𝑟 ∈ ( Base ‘ 𝑅 ) ∧ 𝑠 ∈ ( Base ‘ 𝑅 ) ∧ 𝑡 ∈ ( Base ‘ 𝑅 ) ) ) → ( ( 𝑟 ( +g ‘ 𝑅 ) 𝑠 ) ( .r ‘ 𝑅 ) 𝑡 ) = ( ( 𝑟 ( .r ‘ 𝑅 ) 𝑡 ) ( +g ‘ 𝑅 ) ( 𝑠 ( .r ‘ 𝑅 ) 𝑡 ) ) ) |
67 |
59 60 61 63 66
|
caofdir |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 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 ‘ 𝑅 ) 𝑧 ) ) ) |
68 |
59 53 56
|
ofc12 |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) → ( ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } × { 𝑥 } ) ∘f ( +g ‘ 𝑅 ) ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } × { 𝑦 } ) ) = ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } × { ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) } ) ) |
69 |
68
|
oveq1d |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) → ( ( ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } × { 𝑥 } ) ∘f ( +g ‘ 𝑅 ) ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } × { 𝑦 } ) ) ∘f ( .r ‘ 𝑅 ) 𝑧 ) = ( ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } × { ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) } ) ∘f ( .r ‘ 𝑅 ) 𝑧 ) ) |
70 |
58 67 69
|
3eqtr2rd |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) → ( ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } × { ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) } ) ∘f ( .r ‘ 𝑅 ) 𝑧 ) = ( ( 𝑥 ( ·𝑠 ‘ 𝑆 ) 𝑧 ) ∘f ( +g ‘ 𝑅 ) ( 𝑦 ( ·𝑠 ‘ 𝑆 ) 𝑧 ) ) ) |
71 |
16 34
|
ringacl |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) ∈ ( Base ‘ 𝑅 ) ) |
72 |
64 53 56 71
|
syl3anc |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) → ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) ∈ ( Base ‘ 𝑅 ) ) |
73 |
1 15 16 17 35 28 72 54
|
psrvsca |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) → ( ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) ( ·𝑠 ‘ 𝑆 ) 𝑧 ) = ( ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } × { ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) } ) ∘f ( .r ‘ 𝑅 ) 𝑧 ) ) |
74 |
1 15 16 17 64 53 54
|
psrvscacl |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) → ( 𝑥 ( ·𝑠 ‘ 𝑆 ) 𝑧 ) ∈ ( Base ‘ 𝑆 ) ) |
75 |
1 15 16 17 64 56 54
|
psrvscacl |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) → ( 𝑦 ( ·𝑠 ‘ 𝑆 ) 𝑧 ) ∈ ( Base ‘ 𝑆 ) ) |
76 |
1 17 34 39 74 75
|
psradd |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) → ( ( 𝑥 ( ·𝑠 ‘ 𝑆 ) 𝑧 ) ( +g ‘ 𝑆 ) ( 𝑦 ( ·𝑠 ‘ 𝑆 ) 𝑧 ) ) = ( ( 𝑥 ( ·𝑠 ‘ 𝑆 ) 𝑧 ) ∘f ( +g ‘ 𝑅 ) ( 𝑦 ( ·𝑠 ‘ 𝑆 ) 𝑧 ) ) ) |
77 |
70 73 76
|
3eqtr4d |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) → ( ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) ( ·𝑠 ‘ 𝑆 ) 𝑧 ) = ( ( 𝑥 ( ·𝑠 ‘ 𝑆 ) 𝑧 ) ( +g ‘ 𝑆 ) ( 𝑦 ( ·𝑠 ‘ 𝑆 ) 𝑧 ) ) ) |
78 |
57
|
oveq2d |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) → ( ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } × { 𝑥 } ) ∘f ( .r ‘ 𝑅 ) ( 𝑦 ( ·𝑠 ‘ 𝑆 ) 𝑧 ) ) = ( ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } × { 𝑥 } ) ∘f ( .r ‘ 𝑅 ) ( ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } × { 𝑦 } ) ∘f ( .r ‘ 𝑅 ) 𝑧 ) ) ) |
79 |
16 35
|
ringass |
⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑟 ∈ ( Base ‘ 𝑅 ) ∧ 𝑠 ∈ ( Base ‘ 𝑅 ) ∧ 𝑡 ∈ ( Base ‘ 𝑅 ) ) ) → ( ( 𝑟 ( .r ‘ 𝑅 ) 𝑠 ) ( .r ‘ 𝑅 ) 𝑡 ) = ( 𝑟 ( .r ‘ 𝑅 ) ( 𝑠 ( .r ‘ 𝑅 ) 𝑡 ) ) ) |
80 |
64 79
|
sylan |
⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) ∧ ( 𝑟 ∈ ( Base ‘ 𝑅 ) ∧ 𝑠 ∈ ( Base ‘ 𝑅 ) ∧ 𝑡 ∈ ( Base ‘ 𝑅 ) ) ) → ( ( 𝑟 ( .r ‘ 𝑅 ) 𝑠 ) ( .r ‘ 𝑅 ) 𝑡 ) = ( 𝑟 ( .r ‘ 𝑅 ) ( 𝑠 ( .r ‘ 𝑅 ) 𝑡 ) ) ) |
81 |
59 61 63 60 80
|
caofass |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) → ( ( ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } × { 𝑥 } ) ∘f ( .r ‘ 𝑅 ) ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } × { 𝑦 } ) ) ∘f ( .r ‘ 𝑅 ) 𝑧 ) = ( ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } × { 𝑥 } ) ∘f ( .r ‘ 𝑅 ) ( ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } × { 𝑦 } ) ∘f ( .r ‘ 𝑅 ) 𝑧 ) ) ) |
82 |
59 53 56
|
ofc12 |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) → ( ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } × { 𝑥 } ) ∘f ( .r ‘ 𝑅 ) ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } × { 𝑦 } ) ) = ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } × { ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) } ) ) |
83 |
82
|
oveq1d |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) → ( ( ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } × { 𝑥 } ) ∘f ( .r ‘ 𝑅 ) ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } × { 𝑦 } ) ) ∘f ( .r ‘ 𝑅 ) 𝑧 ) = ( ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } × { ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) } ) ∘f ( .r ‘ 𝑅 ) 𝑧 ) ) |
84 |
78 81 83
|
3eqtr2rd |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) → ( ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } × { ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) } ) ∘f ( .r ‘ 𝑅 ) 𝑧 ) = ( ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } × { 𝑥 } ) ∘f ( .r ‘ 𝑅 ) ( 𝑦 ( ·𝑠 ‘ 𝑆 ) 𝑧 ) ) ) |
85 |
16 35
|
ringcl |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ ( Base ‘ 𝑅 ) ) |
86 |
64 53 56 85
|
syl3anc |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) → ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ ( Base ‘ 𝑅 ) ) |
87 |
1 15 16 17 35 28 86 54
|
psrvsca |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) → ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ( ·𝑠 ‘ 𝑆 ) 𝑧 ) = ( ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } × { ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) } ) ∘f ( .r ‘ 𝑅 ) 𝑧 ) ) |
88 |
1 15 16 17 35 28 53 75
|
psrvsca |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) → ( 𝑥 ( ·𝑠 ‘ 𝑆 ) ( 𝑦 ( ·𝑠 ‘ 𝑆 ) 𝑧 ) ) = ( ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } × { 𝑥 } ) ∘f ( .r ‘ 𝑅 ) ( 𝑦 ( ·𝑠 ‘ 𝑆 ) 𝑧 ) ) ) |
89 |
84 87 88
|
3eqtr4d |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) → ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ( ·𝑠 ‘ 𝑆 ) 𝑧 ) = ( 𝑥 ( ·𝑠 ‘ 𝑆 ) ( 𝑦 ( ·𝑠 ‘ 𝑆 ) 𝑧 ) ) ) |
90 |
3
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ) → 𝑅 ∈ Ring ) |
91 |
|
eqid |
⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 ) |
92 |
16 91
|
ringidcl |
⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) ) |
93 |
90 92
|
syl |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ) → ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) ) |
94 |
|
simpr |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ) → 𝑥 ∈ ( Base ‘ 𝑆 ) ) |
95 |
1 15 16 17 35 28 93 94
|
psrvsca |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ) → ( ( 1r ‘ 𝑅 ) ( ·𝑠 ‘ 𝑆 ) 𝑥 ) = ( ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } × { ( 1r ‘ 𝑅 ) } ) ∘f ( .r ‘ 𝑅 ) 𝑥 ) ) |
96 |
23
|
a1i |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ) → { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∈ V ) |
97 |
1 16 28 17 94
|
psrelbas |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ) → 𝑥 : { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝑅 ) ) |
98 |
16 35 91
|
ringlidm |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) → ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) 𝑟 ) = 𝑟 ) |
99 |
90 98
|
sylan |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) → ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) 𝑟 ) = 𝑟 ) |
100 |
96 97 93 99
|
caofid0l |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ) → ( ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } × { ( 1r ‘ 𝑅 ) } ) ∘f ( .r ‘ 𝑅 ) 𝑥 ) = 𝑥 ) |
101 |
95 100
|
eqtrd |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ) → ( ( 1r ‘ 𝑅 ) ( ·𝑠 ‘ 𝑆 ) 𝑥 ) = 𝑥 ) |
102 |
4 5 6 7 8 9 10 11 3 14 21 52 77 89 101
|
islmodd |
⊢ ( 𝜑 → 𝑆 ∈ LMod ) |