Step |
Hyp |
Ref |
Expression |
1 |
|
psrring.s |
⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 ) |
2 |
|
psrring.i |
⊢ ( 𝜑 → 𝐼 ∈ 𝑉 ) |
3 |
|
psrring.r |
⊢ ( 𝜑 → 𝑅 ∈ Ring ) |
4 |
|
psrass.d |
⊢ 𝐷 = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } |
5 |
|
psrass.t |
⊢ × = ( .r ‘ 𝑆 ) |
6 |
|
psrass.b |
⊢ 𝐵 = ( Base ‘ 𝑆 ) |
7 |
|
psrass.x |
⊢ ( 𝜑 → 𝑋 ∈ 𝐵 ) |
8 |
|
psrass.y |
⊢ ( 𝜑 → 𝑌 ∈ 𝐵 ) |
9 |
|
psrass.z |
⊢ ( 𝜑 → 𝑍 ∈ 𝐵 ) |
10 |
|
eqid |
⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 ) |
11 |
1 6 5 3 7 8
|
psrmulcl |
⊢ ( 𝜑 → ( 𝑋 × 𝑌 ) ∈ 𝐵 ) |
12 |
1 6 5 3 11 9
|
psrmulcl |
⊢ ( 𝜑 → ( ( 𝑋 × 𝑌 ) × 𝑍 ) ∈ 𝐵 ) |
13 |
1 10 4 6 12
|
psrelbas |
⊢ ( 𝜑 → ( ( 𝑋 × 𝑌 ) × 𝑍 ) : 𝐷 ⟶ ( Base ‘ 𝑅 ) ) |
14 |
13
|
ffnd |
⊢ ( 𝜑 → ( ( 𝑋 × 𝑌 ) × 𝑍 ) Fn 𝐷 ) |
15 |
1 6 5 3 8 9
|
psrmulcl |
⊢ ( 𝜑 → ( 𝑌 × 𝑍 ) ∈ 𝐵 ) |
16 |
1 6 5 3 7 15
|
psrmulcl |
⊢ ( 𝜑 → ( 𝑋 × ( 𝑌 × 𝑍 ) ) ∈ 𝐵 ) |
17 |
1 10 4 6 16
|
psrelbas |
⊢ ( 𝜑 → ( 𝑋 × ( 𝑌 × 𝑍 ) ) : 𝐷 ⟶ ( Base ‘ 𝑅 ) ) |
18 |
17
|
ffnd |
⊢ ( 𝜑 → ( 𝑋 × ( 𝑌 × 𝑍 ) ) Fn 𝐷 ) |
19 |
|
eqid |
⊢ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } = { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } |
20 |
|
simpr |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → 𝑥 ∈ 𝐷 ) |
21 |
|
ringcmn |
⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ CMnd ) |
22 |
3 21
|
syl |
⊢ ( 𝜑 → 𝑅 ∈ CMnd ) |
23 |
22
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → 𝑅 ∈ CMnd ) |
24 |
3
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑗 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) → 𝑅 ∈ Ring ) |
25 |
24
|
adantr |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑗 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) ∧ 𝑛 ∈ { ℎ ∈ 𝐷 ∣ ℎ ∘r ≤ ( 𝑥 ∘f − 𝑗 ) } ) → 𝑅 ∈ Ring ) |
26 |
1 10 4 6 7
|
psrelbas |
⊢ ( 𝜑 → 𝑋 : 𝐷 ⟶ ( Base ‘ 𝑅 ) ) |
27 |
26
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑗 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) → 𝑋 : 𝐷 ⟶ ( Base ‘ 𝑅 ) ) |
28 |
|
simpr |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑗 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) → 𝑗 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) |
29 |
|
breq1 |
⊢ ( 𝑔 = 𝑗 → ( 𝑔 ∘r ≤ 𝑥 ↔ 𝑗 ∘r ≤ 𝑥 ) ) |
30 |
29
|
elrab |
⊢ ( 𝑗 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ↔ ( 𝑗 ∈ 𝐷 ∧ 𝑗 ∘r ≤ 𝑥 ) ) |
31 |
28 30
|
sylib |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑗 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) → ( 𝑗 ∈ 𝐷 ∧ 𝑗 ∘r ≤ 𝑥 ) ) |
32 |
31
|
simpld |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑗 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) → 𝑗 ∈ 𝐷 ) |
33 |
27 32
|
ffvelrnd |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑗 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) → ( 𝑋 ‘ 𝑗 ) ∈ ( Base ‘ 𝑅 ) ) |
34 |
33
|
adantr |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑗 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) ∧ 𝑛 ∈ { ℎ ∈ 𝐷 ∣ ℎ ∘r ≤ ( 𝑥 ∘f − 𝑗 ) } ) → ( 𝑋 ‘ 𝑗 ) ∈ ( Base ‘ 𝑅 ) ) |
35 |
1 10 4 6 8
|
psrelbas |
⊢ ( 𝜑 → 𝑌 : 𝐷 ⟶ ( Base ‘ 𝑅 ) ) |
36 |
35
|
ad3antrrr |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑗 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) ∧ 𝑛 ∈ { ℎ ∈ 𝐷 ∣ ℎ ∘r ≤ ( 𝑥 ∘f − 𝑗 ) } ) → 𝑌 : 𝐷 ⟶ ( Base ‘ 𝑅 ) ) |
37 |
|
simpr |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑗 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) ∧ 𝑛 ∈ { ℎ ∈ 𝐷 ∣ ℎ ∘r ≤ ( 𝑥 ∘f − 𝑗 ) } ) → 𝑛 ∈ { ℎ ∈ 𝐷 ∣ ℎ ∘r ≤ ( 𝑥 ∘f − 𝑗 ) } ) |
38 |
|
breq1 |
⊢ ( ℎ = 𝑛 → ( ℎ ∘r ≤ ( 𝑥 ∘f − 𝑗 ) ↔ 𝑛 ∘r ≤ ( 𝑥 ∘f − 𝑗 ) ) ) |
39 |
38
|
elrab |
⊢ ( 𝑛 ∈ { ℎ ∈ 𝐷 ∣ ℎ ∘r ≤ ( 𝑥 ∘f − 𝑗 ) } ↔ ( 𝑛 ∈ 𝐷 ∧ 𝑛 ∘r ≤ ( 𝑥 ∘f − 𝑗 ) ) ) |
40 |
37 39
|
sylib |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑗 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) ∧ 𝑛 ∈ { ℎ ∈ 𝐷 ∣ ℎ ∘r ≤ ( 𝑥 ∘f − 𝑗 ) } ) → ( 𝑛 ∈ 𝐷 ∧ 𝑛 ∘r ≤ ( 𝑥 ∘f − 𝑗 ) ) ) |
41 |
40
|
simpld |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑗 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) ∧ 𝑛 ∈ { ℎ ∈ 𝐷 ∣ ℎ ∘r ≤ ( 𝑥 ∘f − 𝑗 ) } ) → 𝑛 ∈ 𝐷 ) |
42 |
36 41
|
ffvelrnd |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑗 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) ∧ 𝑛 ∈ { ℎ ∈ 𝐷 ∣ ℎ ∘r ≤ ( 𝑥 ∘f − 𝑗 ) } ) → ( 𝑌 ‘ 𝑛 ) ∈ ( Base ‘ 𝑅 ) ) |
43 |
1 10 4 6 9
|
psrelbas |
⊢ ( 𝜑 → 𝑍 : 𝐷 ⟶ ( Base ‘ 𝑅 ) ) |
44 |
43
|
ad3antrrr |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑗 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) ∧ 𝑛 ∈ { ℎ ∈ 𝐷 ∣ ℎ ∘r ≤ ( 𝑥 ∘f − 𝑗 ) } ) → 𝑍 : 𝐷 ⟶ ( Base ‘ 𝑅 ) ) |
45 |
|
simplr |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑗 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) → 𝑥 ∈ 𝐷 ) |
46 |
4
|
psrbagf |
⊢ ( 𝑗 ∈ 𝐷 → 𝑗 : 𝐼 ⟶ ℕ0 ) |
47 |
32 46
|
syl |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑗 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) → 𝑗 : 𝐼 ⟶ ℕ0 ) |
48 |
31
|
simprd |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑗 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) → 𝑗 ∘r ≤ 𝑥 ) |
49 |
4
|
psrbagcon |
⊢ ( ( 𝑥 ∈ 𝐷 ∧ 𝑗 : 𝐼 ⟶ ℕ0 ∧ 𝑗 ∘r ≤ 𝑥 ) → ( ( 𝑥 ∘f − 𝑗 ) ∈ 𝐷 ∧ ( 𝑥 ∘f − 𝑗 ) ∘r ≤ 𝑥 ) ) |
50 |
45 47 48 49
|
syl3anc |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑗 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) → ( ( 𝑥 ∘f − 𝑗 ) ∈ 𝐷 ∧ ( 𝑥 ∘f − 𝑗 ) ∘r ≤ 𝑥 ) ) |
51 |
50
|
simpld |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑗 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) → ( 𝑥 ∘f − 𝑗 ) ∈ 𝐷 ) |
52 |
51
|
adantr |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑗 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) ∧ 𝑛 ∈ { ℎ ∈ 𝐷 ∣ ℎ ∘r ≤ ( 𝑥 ∘f − 𝑗 ) } ) → ( 𝑥 ∘f − 𝑗 ) ∈ 𝐷 ) |
53 |
4
|
psrbagf |
⊢ ( 𝑛 ∈ 𝐷 → 𝑛 : 𝐼 ⟶ ℕ0 ) |
54 |
41 53
|
syl |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑗 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) ∧ 𝑛 ∈ { ℎ ∈ 𝐷 ∣ ℎ ∘r ≤ ( 𝑥 ∘f − 𝑗 ) } ) → 𝑛 : 𝐼 ⟶ ℕ0 ) |
55 |
40
|
simprd |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑗 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) ∧ 𝑛 ∈ { ℎ ∈ 𝐷 ∣ ℎ ∘r ≤ ( 𝑥 ∘f − 𝑗 ) } ) → 𝑛 ∘r ≤ ( 𝑥 ∘f − 𝑗 ) ) |
56 |
4
|
psrbagcon |
⊢ ( ( ( 𝑥 ∘f − 𝑗 ) ∈ 𝐷 ∧ 𝑛 : 𝐼 ⟶ ℕ0 ∧ 𝑛 ∘r ≤ ( 𝑥 ∘f − 𝑗 ) ) → ( ( ( 𝑥 ∘f − 𝑗 ) ∘f − 𝑛 ) ∈ 𝐷 ∧ ( ( 𝑥 ∘f − 𝑗 ) ∘f − 𝑛 ) ∘r ≤ ( 𝑥 ∘f − 𝑗 ) ) ) |
57 |
52 54 55 56
|
syl3anc |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑗 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) ∧ 𝑛 ∈ { ℎ ∈ 𝐷 ∣ ℎ ∘r ≤ ( 𝑥 ∘f − 𝑗 ) } ) → ( ( ( 𝑥 ∘f − 𝑗 ) ∘f − 𝑛 ) ∈ 𝐷 ∧ ( ( 𝑥 ∘f − 𝑗 ) ∘f − 𝑛 ) ∘r ≤ ( 𝑥 ∘f − 𝑗 ) ) ) |
58 |
57
|
simpld |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑗 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) ∧ 𝑛 ∈ { ℎ ∈ 𝐷 ∣ ℎ ∘r ≤ ( 𝑥 ∘f − 𝑗 ) } ) → ( ( 𝑥 ∘f − 𝑗 ) ∘f − 𝑛 ) ∈ 𝐷 ) |
59 |
44 58
|
ffvelrnd |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑗 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) ∧ 𝑛 ∈ { ℎ ∈ 𝐷 ∣ ℎ ∘r ≤ ( 𝑥 ∘f − 𝑗 ) } ) → ( 𝑍 ‘ ( ( 𝑥 ∘f − 𝑗 ) ∘f − 𝑛 ) ) ∈ ( Base ‘ 𝑅 ) ) |
60 |
|
eqid |
⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 ) |
61 |
10 60
|
ringcl |
⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑌 ‘ 𝑛 ) ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑍 ‘ ( ( 𝑥 ∘f − 𝑗 ) ∘f − 𝑛 ) ) ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝑌 ‘ 𝑛 ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( ( 𝑥 ∘f − 𝑗 ) ∘f − 𝑛 ) ) ) ∈ ( Base ‘ 𝑅 ) ) |
62 |
25 42 59 61
|
syl3anc |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑗 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) ∧ 𝑛 ∈ { ℎ ∈ 𝐷 ∣ ℎ ∘r ≤ ( 𝑥 ∘f − 𝑗 ) } ) → ( ( 𝑌 ‘ 𝑛 ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( ( 𝑥 ∘f − 𝑗 ) ∘f − 𝑛 ) ) ) ∈ ( Base ‘ 𝑅 ) ) |
63 |
10 60
|
ringcl |
⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ‘ 𝑗 ) ∈ ( Base ‘ 𝑅 ) ∧ ( ( 𝑌 ‘ 𝑛 ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( ( 𝑥 ∘f − 𝑗 ) ∘f − 𝑛 ) ) ) ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝑋 ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( ( 𝑌 ‘ 𝑛 ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( ( 𝑥 ∘f − 𝑗 ) ∘f − 𝑛 ) ) ) ) ∈ ( Base ‘ 𝑅 ) ) |
64 |
25 34 62 63
|
syl3anc |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑗 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) ∧ 𝑛 ∈ { ℎ ∈ 𝐷 ∣ ℎ ∘r ≤ ( 𝑥 ∘f − 𝑗 ) } ) → ( ( 𝑋 ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( ( 𝑌 ‘ 𝑛 ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( ( 𝑥 ∘f − 𝑗 ) ∘f − 𝑛 ) ) ) ) ∈ ( Base ‘ 𝑅 ) ) |
65 |
64
|
anasss |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝑗 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ∧ 𝑛 ∈ { ℎ ∈ 𝐷 ∣ ℎ ∘r ≤ ( 𝑥 ∘f − 𝑗 ) } ) ) → ( ( 𝑋 ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( ( 𝑌 ‘ 𝑛 ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( ( 𝑥 ∘f − 𝑗 ) ∘f − 𝑛 ) ) ) ) ∈ ( Base ‘ 𝑅 ) ) |
66 |
|
fveq2 |
⊢ ( 𝑛 = ( 𝑘 ∘f − 𝑗 ) → ( 𝑌 ‘ 𝑛 ) = ( 𝑌 ‘ ( 𝑘 ∘f − 𝑗 ) ) ) |
67 |
|
oveq2 |
⊢ ( 𝑛 = ( 𝑘 ∘f − 𝑗 ) → ( ( 𝑥 ∘f − 𝑗 ) ∘f − 𝑛 ) = ( ( 𝑥 ∘f − 𝑗 ) ∘f − ( 𝑘 ∘f − 𝑗 ) ) ) |
68 |
67
|
fveq2d |
⊢ ( 𝑛 = ( 𝑘 ∘f − 𝑗 ) → ( 𝑍 ‘ ( ( 𝑥 ∘f − 𝑗 ) ∘f − 𝑛 ) ) = ( 𝑍 ‘ ( ( 𝑥 ∘f − 𝑗 ) ∘f − ( 𝑘 ∘f − 𝑗 ) ) ) ) |
69 |
66 68
|
oveq12d |
⊢ ( 𝑛 = ( 𝑘 ∘f − 𝑗 ) → ( ( 𝑌 ‘ 𝑛 ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( ( 𝑥 ∘f − 𝑗 ) ∘f − 𝑛 ) ) ) = ( ( 𝑌 ‘ ( 𝑘 ∘f − 𝑗 ) ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( ( 𝑥 ∘f − 𝑗 ) ∘f − ( 𝑘 ∘f − 𝑗 ) ) ) ) ) |
70 |
69
|
oveq2d |
⊢ ( 𝑛 = ( 𝑘 ∘f − 𝑗 ) → ( ( 𝑋 ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( ( 𝑌 ‘ 𝑛 ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( ( 𝑥 ∘f − 𝑗 ) ∘f − 𝑛 ) ) ) ) = ( ( 𝑋 ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( ( 𝑌 ‘ ( 𝑘 ∘f − 𝑗 ) ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( ( 𝑥 ∘f − 𝑗 ) ∘f − ( 𝑘 ∘f − 𝑗 ) ) ) ) ) ) |
71 |
4 19 20 10 23 65 70
|
psrass1lem |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( 𝑅 Σg ( 𝑘 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ↦ ( 𝑅 Σg ( 𝑗 ∈ { ℎ ∈ 𝐷 ∣ ℎ ∘r ≤ 𝑘 } ↦ ( ( 𝑋 ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( ( 𝑌 ‘ ( 𝑘 ∘f − 𝑗 ) ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( ( 𝑥 ∘f − 𝑗 ) ∘f − ( 𝑘 ∘f − 𝑗 ) ) ) ) ) ) ) ) ) = ( 𝑅 Σg ( 𝑗 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ↦ ( 𝑅 Σg ( 𝑛 ∈ { ℎ ∈ 𝐷 ∣ ℎ ∘r ≤ ( 𝑥 ∘f − 𝑗 ) } ↦ ( ( 𝑋 ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( ( 𝑌 ‘ 𝑛 ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( ( 𝑥 ∘f − 𝑗 ) ∘f − 𝑛 ) ) ) ) ) ) ) ) ) |
72 |
7
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑘 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) → 𝑋 ∈ 𝐵 ) |
73 |
8
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑘 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) → 𝑌 ∈ 𝐵 ) |
74 |
|
simpr |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑘 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) → 𝑘 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) |
75 |
|
breq1 |
⊢ ( 𝑔 = 𝑘 → ( 𝑔 ∘r ≤ 𝑥 ↔ 𝑘 ∘r ≤ 𝑥 ) ) |
76 |
75
|
elrab |
⊢ ( 𝑘 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ↔ ( 𝑘 ∈ 𝐷 ∧ 𝑘 ∘r ≤ 𝑥 ) ) |
77 |
74 76
|
sylib |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑘 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) → ( 𝑘 ∈ 𝐷 ∧ 𝑘 ∘r ≤ 𝑥 ) ) |
78 |
77
|
simpld |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑘 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) → 𝑘 ∈ 𝐷 ) |
79 |
1 6 60 5 4 72 73 78
|
psrmulval |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑘 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) → ( ( 𝑋 × 𝑌 ) ‘ 𝑘 ) = ( 𝑅 Σg ( 𝑗 ∈ { ℎ ∈ 𝐷 ∣ ℎ ∘r ≤ 𝑘 } ↦ ( ( 𝑋 ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑘 ∘f − 𝑗 ) ) ) ) ) ) |
80 |
79
|
oveq1d |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑘 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) → ( ( ( 𝑋 × 𝑌 ) ‘ 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( 𝑥 ∘f − 𝑘 ) ) ) = ( ( 𝑅 Σg ( 𝑗 ∈ { ℎ ∈ 𝐷 ∣ ℎ ∘r ≤ 𝑘 } ↦ ( ( 𝑋 ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑘 ∘f − 𝑗 ) ) ) ) ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( 𝑥 ∘f − 𝑘 ) ) ) ) |
81 |
|
eqid |
⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 ) |
82 |
|
eqid |
⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 ) |
83 |
3
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑘 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) → 𝑅 ∈ Ring ) |
84 |
4
|
psrbaglefi |
⊢ ( 𝑘 ∈ 𝐷 → { ℎ ∈ 𝐷 ∣ ℎ ∘r ≤ 𝑘 } ∈ Fin ) |
85 |
78 84
|
syl |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑘 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) → { ℎ ∈ 𝐷 ∣ ℎ ∘r ≤ 𝑘 } ∈ Fin ) |
86 |
43
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑘 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) → 𝑍 : 𝐷 ⟶ ( Base ‘ 𝑅 ) ) |
87 |
|
simplr |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑘 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) → 𝑥 ∈ 𝐷 ) |
88 |
4
|
psrbagf |
⊢ ( 𝑘 ∈ 𝐷 → 𝑘 : 𝐼 ⟶ ℕ0 ) |
89 |
78 88
|
syl |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑘 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) → 𝑘 : 𝐼 ⟶ ℕ0 ) |
90 |
77
|
simprd |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑘 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) → 𝑘 ∘r ≤ 𝑥 ) |
91 |
4
|
psrbagcon |
⊢ ( ( 𝑥 ∈ 𝐷 ∧ 𝑘 : 𝐼 ⟶ ℕ0 ∧ 𝑘 ∘r ≤ 𝑥 ) → ( ( 𝑥 ∘f − 𝑘 ) ∈ 𝐷 ∧ ( 𝑥 ∘f − 𝑘 ) ∘r ≤ 𝑥 ) ) |
92 |
87 89 90 91
|
syl3anc |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑘 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) → ( ( 𝑥 ∘f − 𝑘 ) ∈ 𝐷 ∧ ( 𝑥 ∘f − 𝑘 ) ∘r ≤ 𝑥 ) ) |
93 |
92
|
simpld |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑘 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) → ( 𝑥 ∘f − 𝑘 ) ∈ 𝐷 ) |
94 |
86 93
|
ffvelrnd |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑘 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) → ( 𝑍 ‘ ( 𝑥 ∘f − 𝑘 ) ) ∈ ( Base ‘ 𝑅 ) ) |
95 |
83
|
adantr |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑘 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) ∧ 𝑗 ∈ { ℎ ∈ 𝐷 ∣ ℎ ∘r ≤ 𝑘 } ) → 𝑅 ∈ Ring ) |
96 |
26
|
ad3antrrr |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑘 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) ∧ 𝑗 ∈ { ℎ ∈ 𝐷 ∣ ℎ ∘r ≤ 𝑘 } ) → 𝑋 : 𝐷 ⟶ ( Base ‘ 𝑅 ) ) |
97 |
|
simpr |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑘 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) ∧ 𝑗 ∈ { ℎ ∈ 𝐷 ∣ ℎ ∘r ≤ 𝑘 } ) → 𝑗 ∈ { ℎ ∈ 𝐷 ∣ ℎ ∘r ≤ 𝑘 } ) |
98 |
|
breq1 |
⊢ ( ℎ = 𝑗 → ( ℎ ∘r ≤ 𝑘 ↔ 𝑗 ∘r ≤ 𝑘 ) ) |
99 |
98
|
elrab |
⊢ ( 𝑗 ∈ { ℎ ∈ 𝐷 ∣ ℎ ∘r ≤ 𝑘 } ↔ ( 𝑗 ∈ 𝐷 ∧ 𝑗 ∘r ≤ 𝑘 ) ) |
100 |
97 99
|
sylib |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑘 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) ∧ 𝑗 ∈ { ℎ ∈ 𝐷 ∣ ℎ ∘r ≤ 𝑘 } ) → ( 𝑗 ∈ 𝐷 ∧ 𝑗 ∘r ≤ 𝑘 ) ) |
101 |
100
|
simpld |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑘 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) ∧ 𝑗 ∈ { ℎ ∈ 𝐷 ∣ ℎ ∘r ≤ 𝑘 } ) → 𝑗 ∈ 𝐷 ) |
102 |
96 101
|
ffvelrnd |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑘 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) ∧ 𝑗 ∈ { ℎ ∈ 𝐷 ∣ ℎ ∘r ≤ 𝑘 } ) → ( 𝑋 ‘ 𝑗 ) ∈ ( Base ‘ 𝑅 ) ) |
103 |
35
|
ad3antrrr |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑘 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) ∧ 𝑗 ∈ { ℎ ∈ 𝐷 ∣ ℎ ∘r ≤ 𝑘 } ) → 𝑌 : 𝐷 ⟶ ( Base ‘ 𝑅 ) ) |
104 |
78
|
adantr |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑘 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) ∧ 𝑗 ∈ { ℎ ∈ 𝐷 ∣ ℎ ∘r ≤ 𝑘 } ) → 𝑘 ∈ 𝐷 ) |
105 |
101 46
|
syl |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑘 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) ∧ 𝑗 ∈ { ℎ ∈ 𝐷 ∣ ℎ ∘r ≤ 𝑘 } ) → 𝑗 : 𝐼 ⟶ ℕ0 ) |
106 |
100
|
simprd |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑘 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) ∧ 𝑗 ∈ { ℎ ∈ 𝐷 ∣ ℎ ∘r ≤ 𝑘 } ) → 𝑗 ∘r ≤ 𝑘 ) |
107 |
4
|
psrbagcon |
⊢ ( ( 𝑘 ∈ 𝐷 ∧ 𝑗 : 𝐼 ⟶ ℕ0 ∧ 𝑗 ∘r ≤ 𝑘 ) → ( ( 𝑘 ∘f − 𝑗 ) ∈ 𝐷 ∧ ( 𝑘 ∘f − 𝑗 ) ∘r ≤ 𝑘 ) ) |
108 |
104 105 106 107
|
syl3anc |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑘 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) ∧ 𝑗 ∈ { ℎ ∈ 𝐷 ∣ ℎ ∘r ≤ 𝑘 } ) → ( ( 𝑘 ∘f − 𝑗 ) ∈ 𝐷 ∧ ( 𝑘 ∘f − 𝑗 ) ∘r ≤ 𝑘 ) ) |
109 |
108
|
simpld |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑘 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) ∧ 𝑗 ∈ { ℎ ∈ 𝐷 ∣ ℎ ∘r ≤ 𝑘 } ) → ( 𝑘 ∘f − 𝑗 ) ∈ 𝐷 ) |
110 |
103 109
|
ffvelrnd |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑘 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) ∧ 𝑗 ∈ { ℎ ∈ 𝐷 ∣ ℎ ∘r ≤ 𝑘 } ) → ( 𝑌 ‘ ( 𝑘 ∘f − 𝑗 ) ) ∈ ( Base ‘ 𝑅 ) ) |
111 |
10 60
|
ringcl |
⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ‘ 𝑗 ) ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑌 ‘ ( 𝑘 ∘f − 𝑗 ) ) ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝑋 ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑘 ∘f − 𝑗 ) ) ) ∈ ( Base ‘ 𝑅 ) ) |
112 |
95 102 110 111
|
syl3anc |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑘 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) ∧ 𝑗 ∈ { ℎ ∈ 𝐷 ∣ ℎ ∘r ≤ 𝑘 } ) → ( ( 𝑋 ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑘 ∘f − 𝑗 ) ) ) ∈ ( Base ‘ 𝑅 ) ) |
113 |
|
eqid |
⊢ ( 𝑗 ∈ { ℎ ∈ 𝐷 ∣ ℎ ∘r ≤ 𝑘 } ↦ ( ( 𝑋 ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑘 ∘f − 𝑗 ) ) ) ) = ( 𝑗 ∈ { ℎ ∈ 𝐷 ∣ ℎ ∘r ≤ 𝑘 } ↦ ( ( 𝑋 ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑘 ∘f − 𝑗 ) ) ) ) |
114 |
|
fvex |
⊢ ( 0g ‘ 𝑅 ) ∈ V |
115 |
114
|
a1i |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑘 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) → ( 0g ‘ 𝑅 ) ∈ V ) |
116 |
113 85 112 115
|
fsuppmptdm |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑘 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) → ( 𝑗 ∈ { ℎ ∈ 𝐷 ∣ ℎ ∘r ≤ 𝑘 } ↦ ( ( 𝑋 ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑘 ∘f − 𝑗 ) ) ) ) finSupp ( 0g ‘ 𝑅 ) ) |
117 |
10 81 82 60 83 85 94 112 116
|
gsummulc1 |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑘 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) → ( 𝑅 Σg ( 𝑗 ∈ { ℎ ∈ 𝐷 ∣ ℎ ∘r ≤ 𝑘 } ↦ ( ( ( 𝑋 ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑘 ∘f − 𝑗 ) ) ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( 𝑥 ∘f − 𝑘 ) ) ) ) ) = ( ( 𝑅 Σg ( 𝑗 ∈ { ℎ ∈ 𝐷 ∣ ℎ ∘r ≤ 𝑘 } ↦ ( ( 𝑋 ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑘 ∘f − 𝑗 ) ) ) ) ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( 𝑥 ∘f − 𝑘 ) ) ) ) |
118 |
94
|
adantr |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑘 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) ∧ 𝑗 ∈ { ℎ ∈ 𝐷 ∣ ℎ ∘r ≤ 𝑘 } ) → ( 𝑍 ‘ ( 𝑥 ∘f − 𝑘 ) ) ∈ ( Base ‘ 𝑅 ) ) |
119 |
10 60
|
ringass |
⊢ ( ( 𝑅 ∈ Ring ∧ ( ( 𝑋 ‘ 𝑗 ) ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑌 ‘ ( 𝑘 ∘f − 𝑗 ) ) ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑍 ‘ ( 𝑥 ∘f − 𝑘 ) ) ∈ ( Base ‘ 𝑅 ) ) ) → ( ( ( 𝑋 ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑘 ∘f − 𝑗 ) ) ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( 𝑥 ∘f − 𝑘 ) ) ) = ( ( 𝑋 ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( ( 𝑌 ‘ ( 𝑘 ∘f − 𝑗 ) ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( 𝑥 ∘f − 𝑘 ) ) ) ) ) |
120 |
95 102 110 118 119
|
syl13anc |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑘 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) ∧ 𝑗 ∈ { ℎ ∈ 𝐷 ∣ ℎ ∘r ≤ 𝑘 } ) → ( ( ( 𝑋 ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑘 ∘f − 𝑗 ) ) ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( 𝑥 ∘f − 𝑘 ) ) ) = ( ( 𝑋 ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( ( 𝑌 ‘ ( 𝑘 ∘f − 𝑗 ) ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( 𝑥 ∘f − 𝑘 ) ) ) ) ) |
121 |
4
|
psrbagf |
⊢ ( 𝑥 ∈ 𝐷 → 𝑥 : 𝐼 ⟶ ℕ0 ) |
122 |
121
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → 𝑥 : 𝐼 ⟶ ℕ0 ) |
123 |
122
|
ad2antrr |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑘 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) ∧ 𝑗 ∈ { ℎ ∈ 𝐷 ∣ ℎ ∘r ≤ 𝑘 } ) → 𝑥 : 𝐼 ⟶ ℕ0 ) |
124 |
123
|
ffvelrnda |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑘 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) ∧ 𝑗 ∈ { ℎ ∈ 𝐷 ∣ ℎ ∘r ≤ 𝑘 } ) ∧ 𝑧 ∈ 𝐼 ) → ( 𝑥 ‘ 𝑧 ) ∈ ℕ0 ) |
125 |
89
|
adantr |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑘 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) ∧ 𝑗 ∈ { ℎ ∈ 𝐷 ∣ ℎ ∘r ≤ 𝑘 } ) → 𝑘 : 𝐼 ⟶ ℕ0 ) |
126 |
125
|
ffvelrnda |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑘 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) ∧ 𝑗 ∈ { ℎ ∈ 𝐷 ∣ ℎ ∘r ≤ 𝑘 } ) ∧ 𝑧 ∈ 𝐼 ) → ( 𝑘 ‘ 𝑧 ) ∈ ℕ0 ) |
127 |
105
|
ffvelrnda |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑘 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) ∧ 𝑗 ∈ { ℎ ∈ 𝐷 ∣ ℎ ∘r ≤ 𝑘 } ) ∧ 𝑧 ∈ 𝐼 ) → ( 𝑗 ‘ 𝑧 ) ∈ ℕ0 ) |
128 |
|
nn0cn |
⊢ ( ( 𝑥 ‘ 𝑧 ) ∈ ℕ0 → ( 𝑥 ‘ 𝑧 ) ∈ ℂ ) |
129 |
|
nn0cn |
⊢ ( ( 𝑘 ‘ 𝑧 ) ∈ ℕ0 → ( 𝑘 ‘ 𝑧 ) ∈ ℂ ) |
130 |
|
nn0cn |
⊢ ( ( 𝑗 ‘ 𝑧 ) ∈ ℕ0 → ( 𝑗 ‘ 𝑧 ) ∈ ℂ ) |
131 |
|
nnncan2 |
⊢ ( ( ( 𝑥 ‘ 𝑧 ) ∈ ℂ ∧ ( 𝑘 ‘ 𝑧 ) ∈ ℂ ∧ ( 𝑗 ‘ 𝑧 ) ∈ ℂ ) → ( ( ( 𝑥 ‘ 𝑧 ) − ( 𝑗 ‘ 𝑧 ) ) − ( ( 𝑘 ‘ 𝑧 ) − ( 𝑗 ‘ 𝑧 ) ) ) = ( ( 𝑥 ‘ 𝑧 ) − ( 𝑘 ‘ 𝑧 ) ) ) |
132 |
128 129 130 131
|
syl3an |
⊢ ( ( ( 𝑥 ‘ 𝑧 ) ∈ ℕ0 ∧ ( 𝑘 ‘ 𝑧 ) ∈ ℕ0 ∧ ( 𝑗 ‘ 𝑧 ) ∈ ℕ0 ) → ( ( ( 𝑥 ‘ 𝑧 ) − ( 𝑗 ‘ 𝑧 ) ) − ( ( 𝑘 ‘ 𝑧 ) − ( 𝑗 ‘ 𝑧 ) ) ) = ( ( 𝑥 ‘ 𝑧 ) − ( 𝑘 ‘ 𝑧 ) ) ) |
133 |
124 126 127 132
|
syl3anc |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑘 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) ∧ 𝑗 ∈ { ℎ ∈ 𝐷 ∣ ℎ ∘r ≤ 𝑘 } ) ∧ 𝑧 ∈ 𝐼 ) → ( ( ( 𝑥 ‘ 𝑧 ) − ( 𝑗 ‘ 𝑧 ) ) − ( ( 𝑘 ‘ 𝑧 ) − ( 𝑗 ‘ 𝑧 ) ) ) = ( ( 𝑥 ‘ 𝑧 ) − ( 𝑘 ‘ 𝑧 ) ) ) |
134 |
133
|
mpteq2dva |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑘 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) ∧ 𝑗 ∈ { ℎ ∈ 𝐷 ∣ ℎ ∘r ≤ 𝑘 } ) → ( 𝑧 ∈ 𝐼 ↦ ( ( ( 𝑥 ‘ 𝑧 ) − ( 𝑗 ‘ 𝑧 ) ) − ( ( 𝑘 ‘ 𝑧 ) − ( 𝑗 ‘ 𝑧 ) ) ) ) = ( 𝑧 ∈ 𝐼 ↦ ( ( 𝑥 ‘ 𝑧 ) − ( 𝑘 ‘ 𝑧 ) ) ) ) |
135 |
2
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑘 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) → 𝐼 ∈ 𝑉 ) |
136 |
135
|
adantr |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑘 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) ∧ 𝑗 ∈ { ℎ ∈ 𝐷 ∣ ℎ ∘r ≤ 𝑘 } ) → 𝐼 ∈ 𝑉 ) |
137 |
|
ovexd |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑘 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) ∧ 𝑗 ∈ { ℎ ∈ 𝐷 ∣ ℎ ∘r ≤ 𝑘 } ) ∧ 𝑧 ∈ 𝐼 ) → ( ( 𝑥 ‘ 𝑧 ) − ( 𝑗 ‘ 𝑧 ) ) ∈ V ) |
138 |
|
ovexd |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑘 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) ∧ 𝑗 ∈ { ℎ ∈ 𝐷 ∣ ℎ ∘r ≤ 𝑘 } ) ∧ 𝑧 ∈ 𝐼 ) → ( ( 𝑘 ‘ 𝑧 ) − ( 𝑗 ‘ 𝑧 ) ) ∈ V ) |
139 |
123
|
feqmptd |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑘 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) ∧ 𝑗 ∈ { ℎ ∈ 𝐷 ∣ ℎ ∘r ≤ 𝑘 } ) → 𝑥 = ( 𝑧 ∈ 𝐼 ↦ ( 𝑥 ‘ 𝑧 ) ) ) |
140 |
105
|
feqmptd |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑘 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) ∧ 𝑗 ∈ { ℎ ∈ 𝐷 ∣ ℎ ∘r ≤ 𝑘 } ) → 𝑗 = ( 𝑧 ∈ 𝐼 ↦ ( 𝑗 ‘ 𝑧 ) ) ) |
141 |
136 124 127 139 140
|
offval2 |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑘 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) ∧ 𝑗 ∈ { ℎ ∈ 𝐷 ∣ ℎ ∘r ≤ 𝑘 } ) → ( 𝑥 ∘f − 𝑗 ) = ( 𝑧 ∈ 𝐼 ↦ ( ( 𝑥 ‘ 𝑧 ) − ( 𝑗 ‘ 𝑧 ) ) ) ) |
142 |
125
|
feqmptd |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑘 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) ∧ 𝑗 ∈ { ℎ ∈ 𝐷 ∣ ℎ ∘r ≤ 𝑘 } ) → 𝑘 = ( 𝑧 ∈ 𝐼 ↦ ( 𝑘 ‘ 𝑧 ) ) ) |
143 |
136 126 127 142 140
|
offval2 |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑘 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) ∧ 𝑗 ∈ { ℎ ∈ 𝐷 ∣ ℎ ∘r ≤ 𝑘 } ) → ( 𝑘 ∘f − 𝑗 ) = ( 𝑧 ∈ 𝐼 ↦ ( ( 𝑘 ‘ 𝑧 ) − ( 𝑗 ‘ 𝑧 ) ) ) ) |
144 |
136 137 138 141 143
|
offval2 |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑘 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) ∧ 𝑗 ∈ { ℎ ∈ 𝐷 ∣ ℎ ∘r ≤ 𝑘 } ) → ( ( 𝑥 ∘f − 𝑗 ) ∘f − ( 𝑘 ∘f − 𝑗 ) ) = ( 𝑧 ∈ 𝐼 ↦ ( ( ( 𝑥 ‘ 𝑧 ) − ( 𝑗 ‘ 𝑧 ) ) − ( ( 𝑘 ‘ 𝑧 ) − ( 𝑗 ‘ 𝑧 ) ) ) ) ) |
145 |
136 124 126 139 142
|
offval2 |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑘 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) ∧ 𝑗 ∈ { ℎ ∈ 𝐷 ∣ ℎ ∘r ≤ 𝑘 } ) → ( 𝑥 ∘f − 𝑘 ) = ( 𝑧 ∈ 𝐼 ↦ ( ( 𝑥 ‘ 𝑧 ) − ( 𝑘 ‘ 𝑧 ) ) ) ) |
146 |
134 144 145
|
3eqtr4d |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑘 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) ∧ 𝑗 ∈ { ℎ ∈ 𝐷 ∣ ℎ ∘r ≤ 𝑘 } ) → ( ( 𝑥 ∘f − 𝑗 ) ∘f − ( 𝑘 ∘f − 𝑗 ) ) = ( 𝑥 ∘f − 𝑘 ) ) |
147 |
146
|
fveq2d |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑘 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) ∧ 𝑗 ∈ { ℎ ∈ 𝐷 ∣ ℎ ∘r ≤ 𝑘 } ) → ( 𝑍 ‘ ( ( 𝑥 ∘f − 𝑗 ) ∘f − ( 𝑘 ∘f − 𝑗 ) ) ) = ( 𝑍 ‘ ( 𝑥 ∘f − 𝑘 ) ) ) |
148 |
147
|
oveq2d |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑘 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) ∧ 𝑗 ∈ { ℎ ∈ 𝐷 ∣ ℎ ∘r ≤ 𝑘 } ) → ( ( 𝑌 ‘ ( 𝑘 ∘f − 𝑗 ) ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( ( 𝑥 ∘f − 𝑗 ) ∘f − ( 𝑘 ∘f − 𝑗 ) ) ) ) = ( ( 𝑌 ‘ ( 𝑘 ∘f − 𝑗 ) ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( 𝑥 ∘f − 𝑘 ) ) ) ) |
149 |
148
|
oveq2d |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑘 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) ∧ 𝑗 ∈ { ℎ ∈ 𝐷 ∣ ℎ ∘r ≤ 𝑘 } ) → ( ( 𝑋 ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( ( 𝑌 ‘ ( 𝑘 ∘f − 𝑗 ) ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( ( 𝑥 ∘f − 𝑗 ) ∘f − ( 𝑘 ∘f − 𝑗 ) ) ) ) ) = ( ( 𝑋 ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( ( 𝑌 ‘ ( 𝑘 ∘f − 𝑗 ) ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( 𝑥 ∘f − 𝑘 ) ) ) ) ) |
150 |
120 149
|
eqtr4d |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑘 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) ∧ 𝑗 ∈ { ℎ ∈ 𝐷 ∣ ℎ ∘r ≤ 𝑘 } ) → ( ( ( 𝑋 ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑘 ∘f − 𝑗 ) ) ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( 𝑥 ∘f − 𝑘 ) ) ) = ( ( 𝑋 ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( ( 𝑌 ‘ ( 𝑘 ∘f − 𝑗 ) ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( ( 𝑥 ∘f − 𝑗 ) ∘f − ( 𝑘 ∘f − 𝑗 ) ) ) ) ) ) |
151 |
150
|
mpteq2dva |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑘 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) → ( 𝑗 ∈ { ℎ ∈ 𝐷 ∣ ℎ ∘r ≤ 𝑘 } ↦ ( ( ( 𝑋 ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑘 ∘f − 𝑗 ) ) ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( 𝑥 ∘f − 𝑘 ) ) ) ) = ( 𝑗 ∈ { ℎ ∈ 𝐷 ∣ ℎ ∘r ≤ 𝑘 } ↦ ( ( 𝑋 ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( ( 𝑌 ‘ ( 𝑘 ∘f − 𝑗 ) ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( ( 𝑥 ∘f − 𝑗 ) ∘f − ( 𝑘 ∘f − 𝑗 ) ) ) ) ) ) ) |
152 |
151
|
oveq2d |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑘 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) → ( 𝑅 Σg ( 𝑗 ∈ { ℎ ∈ 𝐷 ∣ ℎ ∘r ≤ 𝑘 } ↦ ( ( ( 𝑋 ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑘 ∘f − 𝑗 ) ) ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( 𝑥 ∘f − 𝑘 ) ) ) ) ) = ( 𝑅 Σg ( 𝑗 ∈ { ℎ ∈ 𝐷 ∣ ℎ ∘r ≤ 𝑘 } ↦ ( ( 𝑋 ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( ( 𝑌 ‘ ( 𝑘 ∘f − 𝑗 ) ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( ( 𝑥 ∘f − 𝑗 ) ∘f − ( 𝑘 ∘f − 𝑗 ) ) ) ) ) ) ) ) |
153 |
80 117 152
|
3eqtr2d |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑘 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) → ( ( ( 𝑋 × 𝑌 ) ‘ 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( 𝑥 ∘f − 𝑘 ) ) ) = ( 𝑅 Σg ( 𝑗 ∈ { ℎ ∈ 𝐷 ∣ ℎ ∘r ≤ 𝑘 } ↦ ( ( 𝑋 ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( ( 𝑌 ‘ ( 𝑘 ∘f − 𝑗 ) ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( ( 𝑥 ∘f − 𝑗 ) ∘f − ( 𝑘 ∘f − 𝑗 ) ) ) ) ) ) ) ) |
154 |
153
|
mpteq2dva |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( 𝑘 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ↦ ( ( ( 𝑋 × 𝑌 ) ‘ 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( 𝑥 ∘f − 𝑘 ) ) ) ) = ( 𝑘 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ↦ ( 𝑅 Σg ( 𝑗 ∈ { ℎ ∈ 𝐷 ∣ ℎ ∘r ≤ 𝑘 } ↦ ( ( 𝑋 ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( ( 𝑌 ‘ ( 𝑘 ∘f − 𝑗 ) ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( ( 𝑥 ∘f − 𝑗 ) ∘f − ( 𝑘 ∘f − 𝑗 ) ) ) ) ) ) ) ) ) |
155 |
154
|
oveq2d |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( 𝑅 Σg ( 𝑘 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ↦ ( ( ( 𝑋 × 𝑌 ) ‘ 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( 𝑥 ∘f − 𝑘 ) ) ) ) ) = ( 𝑅 Σg ( 𝑘 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ↦ ( 𝑅 Σg ( 𝑗 ∈ { ℎ ∈ 𝐷 ∣ ℎ ∘r ≤ 𝑘 } ↦ ( ( 𝑋 ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( ( 𝑌 ‘ ( 𝑘 ∘f − 𝑗 ) ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( ( 𝑥 ∘f − 𝑗 ) ∘f − ( 𝑘 ∘f − 𝑗 ) ) ) ) ) ) ) ) ) ) |
156 |
8
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑗 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) → 𝑌 ∈ 𝐵 ) |
157 |
9
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑗 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) → 𝑍 ∈ 𝐵 ) |
158 |
1 6 60 5 4 156 157 51
|
psrmulval |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑗 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) → ( ( 𝑌 × 𝑍 ) ‘ ( 𝑥 ∘f − 𝑗 ) ) = ( 𝑅 Σg ( 𝑛 ∈ { ℎ ∈ 𝐷 ∣ ℎ ∘r ≤ ( 𝑥 ∘f − 𝑗 ) } ↦ ( ( 𝑌 ‘ 𝑛 ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( ( 𝑥 ∘f − 𝑗 ) ∘f − 𝑛 ) ) ) ) ) ) |
159 |
158
|
oveq2d |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑗 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) → ( ( 𝑋 ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( ( 𝑌 × 𝑍 ) ‘ ( 𝑥 ∘f − 𝑗 ) ) ) = ( ( 𝑋 ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑅 Σg ( 𝑛 ∈ { ℎ ∈ 𝐷 ∣ ℎ ∘r ≤ ( 𝑥 ∘f − 𝑗 ) } ↦ ( ( 𝑌 ‘ 𝑛 ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( ( 𝑥 ∘f − 𝑗 ) ∘f − 𝑛 ) ) ) ) ) ) ) |
160 |
4
|
psrbaglefi |
⊢ ( ( 𝑥 ∘f − 𝑗 ) ∈ 𝐷 → { ℎ ∈ 𝐷 ∣ ℎ ∘r ≤ ( 𝑥 ∘f − 𝑗 ) } ∈ Fin ) |
161 |
51 160
|
syl |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑗 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) → { ℎ ∈ 𝐷 ∣ ℎ ∘r ≤ ( 𝑥 ∘f − 𝑗 ) } ∈ Fin ) |
162 |
|
ovex |
⊢ ( ℕ0 ↑m 𝐼 ) ∈ V |
163 |
4 162
|
rab2ex |
⊢ { ℎ ∈ 𝐷 ∣ ℎ ∘r ≤ ( 𝑥 ∘f − 𝑗 ) } ∈ V |
164 |
163
|
mptex |
⊢ ( 𝑛 ∈ { ℎ ∈ 𝐷 ∣ ℎ ∘r ≤ ( 𝑥 ∘f − 𝑗 ) } ↦ ( ( 𝑌 ‘ 𝑛 ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( ( 𝑥 ∘f − 𝑗 ) ∘f − 𝑛 ) ) ) ) ∈ V |
165 |
|
funmpt |
⊢ Fun ( 𝑛 ∈ { ℎ ∈ 𝐷 ∣ ℎ ∘r ≤ ( 𝑥 ∘f − 𝑗 ) } ↦ ( ( 𝑌 ‘ 𝑛 ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( ( 𝑥 ∘f − 𝑗 ) ∘f − 𝑛 ) ) ) ) |
166 |
164 165 114
|
3pm3.2i |
⊢ ( ( 𝑛 ∈ { ℎ ∈ 𝐷 ∣ ℎ ∘r ≤ ( 𝑥 ∘f − 𝑗 ) } ↦ ( ( 𝑌 ‘ 𝑛 ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( ( 𝑥 ∘f − 𝑗 ) ∘f − 𝑛 ) ) ) ) ∈ V ∧ Fun ( 𝑛 ∈ { ℎ ∈ 𝐷 ∣ ℎ ∘r ≤ ( 𝑥 ∘f − 𝑗 ) } ↦ ( ( 𝑌 ‘ 𝑛 ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( ( 𝑥 ∘f − 𝑗 ) ∘f − 𝑛 ) ) ) ) ∧ ( 0g ‘ 𝑅 ) ∈ V ) |
167 |
166
|
a1i |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑗 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) → ( ( 𝑛 ∈ { ℎ ∈ 𝐷 ∣ ℎ ∘r ≤ ( 𝑥 ∘f − 𝑗 ) } ↦ ( ( 𝑌 ‘ 𝑛 ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( ( 𝑥 ∘f − 𝑗 ) ∘f − 𝑛 ) ) ) ) ∈ V ∧ Fun ( 𝑛 ∈ { ℎ ∈ 𝐷 ∣ ℎ ∘r ≤ ( 𝑥 ∘f − 𝑗 ) } ↦ ( ( 𝑌 ‘ 𝑛 ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( ( 𝑥 ∘f − 𝑗 ) ∘f − 𝑛 ) ) ) ) ∧ ( 0g ‘ 𝑅 ) ∈ V ) ) |
168 |
|
suppssdm |
⊢ ( ( 𝑛 ∈ { ℎ ∈ 𝐷 ∣ ℎ ∘r ≤ ( 𝑥 ∘f − 𝑗 ) } ↦ ( ( 𝑌 ‘ 𝑛 ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( ( 𝑥 ∘f − 𝑗 ) ∘f − 𝑛 ) ) ) ) supp ( 0g ‘ 𝑅 ) ) ⊆ dom ( 𝑛 ∈ { ℎ ∈ 𝐷 ∣ ℎ ∘r ≤ ( 𝑥 ∘f − 𝑗 ) } ↦ ( ( 𝑌 ‘ 𝑛 ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( ( 𝑥 ∘f − 𝑗 ) ∘f − 𝑛 ) ) ) ) |
169 |
|
eqid |
⊢ ( 𝑛 ∈ { ℎ ∈ 𝐷 ∣ ℎ ∘r ≤ ( 𝑥 ∘f − 𝑗 ) } ↦ ( ( 𝑌 ‘ 𝑛 ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( ( 𝑥 ∘f − 𝑗 ) ∘f − 𝑛 ) ) ) ) = ( 𝑛 ∈ { ℎ ∈ 𝐷 ∣ ℎ ∘r ≤ ( 𝑥 ∘f − 𝑗 ) } ↦ ( ( 𝑌 ‘ 𝑛 ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( ( 𝑥 ∘f − 𝑗 ) ∘f − 𝑛 ) ) ) ) |
170 |
169
|
dmmptss |
⊢ dom ( 𝑛 ∈ { ℎ ∈ 𝐷 ∣ ℎ ∘r ≤ ( 𝑥 ∘f − 𝑗 ) } ↦ ( ( 𝑌 ‘ 𝑛 ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( ( 𝑥 ∘f − 𝑗 ) ∘f − 𝑛 ) ) ) ) ⊆ { ℎ ∈ 𝐷 ∣ ℎ ∘r ≤ ( 𝑥 ∘f − 𝑗 ) } |
171 |
168 170
|
sstri |
⊢ ( ( 𝑛 ∈ { ℎ ∈ 𝐷 ∣ ℎ ∘r ≤ ( 𝑥 ∘f − 𝑗 ) } ↦ ( ( 𝑌 ‘ 𝑛 ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( ( 𝑥 ∘f − 𝑗 ) ∘f − 𝑛 ) ) ) ) supp ( 0g ‘ 𝑅 ) ) ⊆ { ℎ ∈ 𝐷 ∣ ℎ ∘r ≤ ( 𝑥 ∘f − 𝑗 ) } |
172 |
171
|
a1i |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑗 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) → ( ( 𝑛 ∈ { ℎ ∈ 𝐷 ∣ ℎ ∘r ≤ ( 𝑥 ∘f − 𝑗 ) } ↦ ( ( 𝑌 ‘ 𝑛 ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( ( 𝑥 ∘f − 𝑗 ) ∘f − 𝑛 ) ) ) ) supp ( 0g ‘ 𝑅 ) ) ⊆ { ℎ ∈ 𝐷 ∣ ℎ ∘r ≤ ( 𝑥 ∘f − 𝑗 ) } ) |
173 |
|
suppssfifsupp |
⊢ ( ( ( ( 𝑛 ∈ { ℎ ∈ 𝐷 ∣ ℎ ∘r ≤ ( 𝑥 ∘f − 𝑗 ) } ↦ ( ( 𝑌 ‘ 𝑛 ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( ( 𝑥 ∘f − 𝑗 ) ∘f − 𝑛 ) ) ) ) ∈ V ∧ Fun ( 𝑛 ∈ { ℎ ∈ 𝐷 ∣ ℎ ∘r ≤ ( 𝑥 ∘f − 𝑗 ) } ↦ ( ( 𝑌 ‘ 𝑛 ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( ( 𝑥 ∘f − 𝑗 ) ∘f − 𝑛 ) ) ) ) ∧ ( 0g ‘ 𝑅 ) ∈ V ) ∧ ( { ℎ ∈ 𝐷 ∣ ℎ ∘r ≤ ( 𝑥 ∘f − 𝑗 ) } ∈ Fin ∧ ( ( 𝑛 ∈ { ℎ ∈ 𝐷 ∣ ℎ ∘r ≤ ( 𝑥 ∘f − 𝑗 ) } ↦ ( ( 𝑌 ‘ 𝑛 ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( ( 𝑥 ∘f − 𝑗 ) ∘f − 𝑛 ) ) ) ) supp ( 0g ‘ 𝑅 ) ) ⊆ { ℎ ∈ 𝐷 ∣ ℎ ∘r ≤ ( 𝑥 ∘f − 𝑗 ) } ) ) → ( 𝑛 ∈ { ℎ ∈ 𝐷 ∣ ℎ ∘r ≤ ( 𝑥 ∘f − 𝑗 ) } ↦ ( ( 𝑌 ‘ 𝑛 ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( ( 𝑥 ∘f − 𝑗 ) ∘f − 𝑛 ) ) ) ) finSupp ( 0g ‘ 𝑅 ) ) |
174 |
167 161 172 173
|
syl12anc |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑗 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) → ( 𝑛 ∈ { ℎ ∈ 𝐷 ∣ ℎ ∘r ≤ ( 𝑥 ∘f − 𝑗 ) } ↦ ( ( 𝑌 ‘ 𝑛 ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( ( 𝑥 ∘f − 𝑗 ) ∘f − 𝑛 ) ) ) ) finSupp ( 0g ‘ 𝑅 ) ) |
175 |
10 81 82 60 24 161 33 62 174
|
gsummulc2 |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑗 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) → ( 𝑅 Σg ( 𝑛 ∈ { ℎ ∈ 𝐷 ∣ ℎ ∘r ≤ ( 𝑥 ∘f − 𝑗 ) } ↦ ( ( 𝑋 ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( ( 𝑌 ‘ 𝑛 ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( ( 𝑥 ∘f − 𝑗 ) ∘f − 𝑛 ) ) ) ) ) ) = ( ( 𝑋 ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑅 Σg ( 𝑛 ∈ { ℎ ∈ 𝐷 ∣ ℎ ∘r ≤ ( 𝑥 ∘f − 𝑗 ) } ↦ ( ( 𝑌 ‘ 𝑛 ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( ( 𝑥 ∘f − 𝑗 ) ∘f − 𝑛 ) ) ) ) ) ) ) |
176 |
159 175
|
eqtr4d |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑗 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) → ( ( 𝑋 ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( ( 𝑌 × 𝑍 ) ‘ ( 𝑥 ∘f − 𝑗 ) ) ) = ( 𝑅 Σg ( 𝑛 ∈ { ℎ ∈ 𝐷 ∣ ℎ ∘r ≤ ( 𝑥 ∘f − 𝑗 ) } ↦ ( ( 𝑋 ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( ( 𝑌 ‘ 𝑛 ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( ( 𝑥 ∘f − 𝑗 ) ∘f − 𝑛 ) ) ) ) ) ) ) |
177 |
176
|
mpteq2dva |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( 𝑗 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ↦ ( ( 𝑋 ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( ( 𝑌 × 𝑍 ) ‘ ( 𝑥 ∘f − 𝑗 ) ) ) ) = ( 𝑗 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ↦ ( 𝑅 Σg ( 𝑛 ∈ { ℎ ∈ 𝐷 ∣ ℎ ∘r ≤ ( 𝑥 ∘f − 𝑗 ) } ↦ ( ( 𝑋 ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( ( 𝑌 ‘ 𝑛 ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( ( 𝑥 ∘f − 𝑗 ) ∘f − 𝑛 ) ) ) ) ) ) ) ) |
178 |
177
|
oveq2d |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( 𝑅 Σg ( 𝑗 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ↦ ( ( 𝑋 ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( ( 𝑌 × 𝑍 ) ‘ ( 𝑥 ∘f − 𝑗 ) ) ) ) ) = ( 𝑅 Σg ( 𝑗 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ↦ ( 𝑅 Σg ( 𝑛 ∈ { ℎ ∈ 𝐷 ∣ ℎ ∘r ≤ ( 𝑥 ∘f − 𝑗 ) } ↦ ( ( 𝑋 ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( ( 𝑌 ‘ 𝑛 ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( ( 𝑥 ∘f − 𝑗 ) ∘f − 𝑛 ) ) ) ) ) ) ) ) ) |
179 |
71 155 178
|
3eqtr4d |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( 𝑅 Σg ( 𝑘 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ↦ ( ( ( 𝑋 × 𝑌 ) ‘ 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( 𝑥 ∘f − 𝑘 ) ) ) ) ) = ( 𝑅 Σg ( 𝑗 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ↦ ( ( 𝑋 ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( ( 𝑌 × 𝑍 ) ‘ ( 𝑥 ∘f − 𝑗 ) ) ) ) ) ) |
180 |
11
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( 𝑋 × 𝑌 ) ∈ 𝐵 ) |
181 |
9
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → 𝑍 ∈ 𝐵 ) |
182 |
1 6 60 5 4 180 181 20
|
psrmulval |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( ( ( 𝑋 × 𝑌 ) × 𝑍 ) ‘ 𝑥 ) = ( 𝑅 Σg ( 𝑘 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ↦ ( ( ( 𝑋 × 𝑌 ) ‘ 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑍 ‘ ( 𝑥 ∘f − 𝑘 ) ) ) ) ) ) |
183 |
7
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → 𝑋 ∈ 𝐵 ) |
184 |
15
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( 𝑌 × 𝑍 ) ∈ 𝐵 ) |
185 |
1 6 60 5 4 183 184 20
|
psrmulval |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( ( 𝑋 × ( 𝑌 × 𝑍 ) ) ‘ 𝑥 ) = ( 𝑅 Σg ( 𝑗 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ↦ ( ( 𝑋 ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( ( 𝑌 × 𝑍 ) ‘ ( 𝑥 ∘f − 𝑗 ) ) ) ) ) ) |
186 |
179 182 185
|
3eqtr4d |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( ( ( 𝑋 × 𝑌 ) × 𝑍 ) ‘ 𝑥 ) = ( ( 𝑋 × ( 𝑌 × 𝑍 ) ) ‘ 𝑥 ) ) |
187 |
14 18 186
|
eqfnfvd |
⊢ ( 𝜑 → ( ( 𝑋 × 𝑌 ) × 𝑍 ) = ( 𝑋 × ( 𝑌 × 𝑍 ) ) ) |