This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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