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