Metamath Proof Explorer

Theorem psrass1

Description: Associative identity for the ring of power series. (Contributed by Mario Carneiro, 5-Jan-2015)

Ref Expression
Hypotheses psrring.s ⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
psrring.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
psrring.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
psrass.d ⊢ 𝐷 = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
psrass.t ⊢ × = ( .r ‘ 𝑆 )
psrass.b ⊢ 𝐵 = ( Base ‘ 𝑆 )
psrass.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
psrass.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
psrass.z ⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
Assertion psrass1 ( 𝜑 → ( ( 𝑋 × 𝑌 ) × 𝑍 ) = ( 𝑋 × ( 𝑌 × 𝑍 ) ) )

Proof

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