Metamath Proof Explorer

Theorem psrcom

Description: Commutative law for the ring of power series. (Contributed by Mario Carneiro, 7-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 ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
psrcom.c ⊢ ( 𝜑 → 𝑅 ∈ CRing )
Assertion psrcom ( 𝜑 → ( 𝑋 × 𝑌 ) = ( 𝑌 × 𝑋 ) )

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 psrcom.c ⊢ ( 𝜑 → 𝑅 ∈ CRing )
10 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
11 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
12 ringcmn ⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ CMnd )
13 3 12 syl ⊢ ( 𝜑 → 𝑅 ∈ CMnd )
14 13 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → 𝑅 ∈ CMnd )
15 4 psrbaglefi ⊢ ( 𝑥 ∈ 𝐷 → { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ∈ Fin )
16 15 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ∈ Fin )
17 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑘 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) → 𝑅 ∈ Ring )
18 1 10 4 6 7 psrelbas ⊢ ( 𝜑 → 𝑋 : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
19 18 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑘 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) → 𝑋 : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
20 breq1 ⊢ ( 𝑔 = 𝑘 → ( 𝑔 ∘r ≤ 𝑥 ↔ 𝑘 ∘r ≤ 𝑥 ) )
21 20 elrab ⊢ ( 𝑘 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ↔ ( 𝑘 ∈ 𝐷 ∧ 𝑘 ∘r ≤ 𝑥 ) )
22 21 bilani ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑘 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) → ( 𝑘 ∈ 𝐷 ∧ 𝑘 ∘r ≤ 𝑥 ) )
23 22 simpld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑘 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) → 𝑘 ∈ 𝐷 )
24 19 23 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑘 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) → ( 𝑋 ‘ 𝑘 ) ∈ ( Base ‘ 𝑅 ) )
25 1 10 4 6 8 psrelbas ⊢ ( 𝜑 → 𝑌 : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
26 25 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑘 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) → 𝑌 : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
27 simplr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑘 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) → 𝑥 ∈ 𝐷 )
28 4 psrbagf ⊢ ( 𝑘 ∈ 𝐷 → 𝑘 : 𝐼 ⟶ ℕ0 )
29 23 28 syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑘 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) → 𝑘 : 𝐼 ⟶ ℕ0 )
30 22 simprd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑘 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) → 𝑘 ∘r ≤ 𝑥 )
31 4 psrbagcon ⊢ ( ( 𝑥 ∈ 𝐷 ∧ 𝑘 : 𝐼 ⟶ ℕ0 ∧ 𝑘 ∘r ≤ 𝑥 ) → ( ( 𝑥 ∘f − 𝑘 ) ∈ 𝐷 ∧ ( 𝑥 ∘f − 𝑘 ) ∘r ≤ 𝑥 ) )
32 27 29 30 31 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑘 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) → ( ( 𝑥 ∘f − 𝑘 ) ∈ 𝐷 ∧ ( 𝑥 ∘f − 𝑘 ) ∘r ≤ 𝑥 ) )
33 32 simpld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑘 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) → ( 𝑥 ∘f − 𝑘 ) ∈ 𝐷 )
34 26 33 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑘 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) → ( 𝑌 ‘ ( 𝑥 ∘f − 𝑘 ) ) ∈ ( Base ‘ 𝑅 ) )
35 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
36 10 35 ringcl ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ‘ 𝑘 ) ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑌 ‘ ( 𝑥 ∘f − 𝑘 ) ) ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝑋 ‘ 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑥 ∘f − 𝑘 ) ) ) ∈ ( Base ‘ 𝑅 ) )
37 17 24 34 36 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑘 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) → ( ( 𝑋 ‘ 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑥 ∘f − 𝑘 ) ) ) ∈ ( Base ‘ 𝑅 ) )
38 37 fmpttd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( 𝑘 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ↦ ( ( 𝑋 ‘ 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑥 ∘f − 𝑘 ) ) ) ) : { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ⟶ ( Base ‘ 𝑅 ) )
39 ovex ⊢ ( ℕ0 ↑m 𝐼 ) ∈ V
40 4 39 rabex2 ⊢ 𝐷 ∈ V
41 40 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → 𝐷 ∈ V )
42 rabexg ⊢ ( 𝐷 ∈ V → { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ∈ V )
43 41 42 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ∈ V )
44 43 mptexd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( 𝑘 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ↦ ( ( 𝑋 ‘ 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑥 ∘f − 𝑘 ) ) ) ) ∈ V )
45 funmpt ⊢ Fun ( 𝑘 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ↦ ( ( 𝑋 ‘ 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑥 ∘f − 𝑘 ) ) ) )
46 45 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → Fun ( 𝑘 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ↦ ( ( 𝑋 ‘ 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑥 ∘f − 𝑘 ) ) ) ) )
47 fvexd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( 0g ‘ 𝑅 ) ∈ V )
48 suppssdm ⊢ ( ( 𝑘 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ↦ ( ( 𝑋 ‘ 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑥 ∘f − 𝑘 ) ) ) ) supp ( 0g ‘ 𝑅 ) ) ⊆ dom ( 𝑘 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ↦ ( ( 𝑋 ‘ 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑥 ∘f − 𝑘 ) ) ) )
49 eqid ⊢ ( 𝑘 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ↦ ( ( 𝑋 ‘ 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑥 ∘f − 𝑘 ) ) ) ) = ( 𝑘 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ↦ ( ( 𝑋 ‘ 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑥 ∘f − 𝑘 ) ) ) )
50 49 dmmptss ⊢ dom ( 𝑘 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ↦ ( ( 𝑋 ‘ 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑥 ∘f − 𝑘 ) ) ) ) ⊆ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 }
51 48 50 sstri ⊢ ( ( 𝑘 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ↦ ( ( 𝑋 ‘ 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑥 ∘f − 𝑘 ) ) ) ) supp ( 0g ‘ 𝑅 ) ) ⊆ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 }
52 51 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( ( 𝑘 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ↦ ( ( 𝑋 ‘ 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑥 ∘f − 𝑘 ) ) ) ) supp ( 0g ‘ 𝑅 ) ) ⊆ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } )
53 suppssfifsupp ⊢ ( ( ( ( 𝑘 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ↦ ( ( 𝑋 ‘ 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑥 ∘f − 𝑘 ) ) ) ) ∈ V ∧ Fun ( 𝑘 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ↦ ( ( 𝑋 ‘ 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑥 ∘f − 𝑘 ) ) ) ) ∧ ( 0g ‘ 𝑅 ) ∈ V ) ∧ ( { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ∈ Fin ∧ ( ( 𝑘 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ↦ ( ( 𝑋 ‘ 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑥 ∘f − 𝑘 ) ) ) ) supp ( 0g ‘ 𝑅 ) ) ⊆ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) ) → ( 𝑘 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ↦ ( ( 𝑋 ‘ 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑥 ∘f − 𝑘 ) ) ) ) finSupp ( 0g ‘ 𝑅 ) )
54 44 46 47 16 52 53 syl32anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( 𝑘 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ↦ ( ( 𝑋 ‘ 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑥 ∘f − 𝑘 ) ) ) ) finSupp ( 0g ‘ 𝑅 ) )
55 eqid ⊢ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } = { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 }
56 4 55 psrbagconf1o ⊢ ( 𝑥 ∈ 𝐷 → ( 𝑗 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ↦ ( 𝑥 ∘f − 𝑗 ) ) : { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } –1-1-onto→ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } )
57 56 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( 𝑗 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ↦ ( 𝑥 ∘f − 𝑗 ) ) : { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } –1-1-onto→ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } )
58 10 11 14 16 38 54 57 gsumf1o ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( 𝑅 Σg ( 𝑘 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ↦ ( ( 𝑋 ‘ 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑥 ∘f − 𝑘 ) ) ) ) ) = ( 𝑅 Σg ( ( 𝑘 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ↦ ( ( 𝑋 ‘ 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑥 ∘f − 𝑘 ) ) ) ) ∘ ( 𝑗 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ↦ ( 𝑥 ∘f − 𝑗 ) ) ) ) )
59 simplr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑗 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) → 𝑥 ∈ 𝐷 )
60 simpr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑗 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) → 𝑗 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } )
61 4 55 psrbagconcl ⊢ ( ( 𝑥 ∈ 𝐷 ∧ 𝑗 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) → ( 𝑥 ∘f − 𝑗 ) ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } )
62 59 60 61 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑗 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) → ( 𝑥 ∘f − 𝑗 ) ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } )
63 eqidd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( 𝑗 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ↦ ( 𝑥 ∘f − 𝑗 ) ) = ( 𝑗 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ↦ ( 𝑥 ∘f − 𝑗 ) ) )
64 eqidd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( 𝑘 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ↦ ( ( 𝑋 ‘ 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑥 ∘f − 𝑘 ) ) ) ) = ( 𝑘 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ↦ ( ( 𝑋 ‘ 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑥 ∘f − 𝑘 ) ) ) ) )
65 fveq2 ⊢ ( 𝑘 = ( 𝑥 ∘f − 𝑗 ) → ( 𝑋 ‘ 𝑘 ) = ( 𝑋 ‘ ( 𝑥 ∘f − 𝑗 ) ) )
66 oveq2 ⊢ ( 𝑘 = ( 𝑥 ∘f − 𝑗 ) → ( 𝑥 ∘f − 𝑘 ) = ( 𝑥 ∘f − ( 𝑥 ∘f − 𝑗 ) ) )
67 66 fveq2d ⊢ ( 𝑘 = ( 𝑥 ∘f − 𝑗 ) → ( 𝑌 ‘ ( 𝑥 ∘f − 𝑘 ) ) = ( 𝑌 ‘ ( 𝑥 ∘f − ( 𝑥 ∘f − 𝑗 ) ) ) )
68 65 67 oveq12d ⊢ ( 𝑘 = ( 𝑥 ∘f − 𝑗 ) → ( ( 𝑋 ‘ 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑥 ∘f − 𝑘 ) ) ) = ( ( 𝑋 ‘ ( 𝑥 ∘f − 𝑗 ) ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑥 ∘f − ( 𝑥 ∘f − 𝑗 ) ) ) ) )
69 62 63 64 68 fmptco ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( ( 𝑘 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ↦ ( ( 𝑋 ‘ 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑥 ∘f − 𝑘 ) ) ) ) ∘ ( 𝑗 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ↦ ( 𝑥 ∘f − 𝑗 ) ) ) = ( 𝑗 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ↦ ( ( 𝑋 ‘ ( 𝑥 ∘f − 𝑗 ) ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑥 ∘f − ( 𝑥 ∘f − 𝑗 ) ) ) ) ) )
70 4 psrbagf ⊢ ( 𝑥 ∈ 𝐷 → 𝑥 : 𝐼 ⟶ ℕ0 )
71 70 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → 𝑥 : 𝐼 ⟶ ℕ0 )
72 71 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑗 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) → 𝑥 : 𝐼 ⟶ ℕ0 )
73 72 ffvelcdmda ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑗 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) ∧ 𝑧 ∈ 𝐼 ) → ( 𝑥 ‘ 𝑧 ) ∈ ℕ0 )
74 breq1 ⊢ ( 𝑔 = 𝑗 → ( 𝑔 ∘r ≤ 𝑥 ↔ 𝑗 ∘r ≤ 𝑥 ) )
75 74 elrab ⊢ ( 𝑗 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ↔ ( 𝑗 ∈ 𝐷 ∧ 𝑗 ∘r ≤ 𝑥 ) )
76 75 bilani ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑗 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) → ( 𝑗 ∈ 𝐷 ∧ 𝑗 ∘r ≤ 𝑥 ) )
77 76 simpld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑗 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) → 𝑗 ∈ 𝐷 )
78 4 psrbagf ⊢ ( 𝑗 ∈ 𝐷 → 𝑗 : 𝐼 ⟶ ℕ0 )
79 77 78 syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑗 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) → 𝑗 : 𝐼 ⟶ ℕ0 )
80 79 ffvelcdmda ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑗 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) ∧ 𝑧 ∈ 𝐼 ) → ( 𝑗 ‘ 𝑧 ) ∈ ℕ0 )
81 nn0cn ⊢ ( ( 𝑥 ‘ 𝑧 ) ∈ ℕ0 → ( 𝑥 ‘ 𝑧 ) ∈ ℂ )
82 nn0cn ⊢ ( ( 𝑗 ‘ 𝑧 ) ∈ ℕ0 → ( 𝑗 ‘ 𝑧 ) ∈ ℂ )
83 nncan ⊢ ( ( ( 𝑥 ‘ 𝑧 ) ∈ ℂ ∧ ( 𝑗 ‘ 𝑧 ) ∈ ℂ ) → ( ( 𝑥 ‘ 𝑧 ) − ( ( 𝑥 ‘ 𝑧 ) − ( 𝑗 ‘ 𝑧 ) ) ) = ( 𝑗 ‘ 𝑧 ) )
84 81 82 83 syl2an ⊢ ( ( ( 𝑥 ‘ 𝑧 ) ∈ ℕ0 ∧ ( 𝑗 ‘ 𝑧 ) ∈ ℕ0 ) → ( ( 𝑥 ‘ 𝑧 ) − ( ( 𝑥 ‘ 𝑧 ) − ( 𝑗 ‘ 𝑧 ) ) ) = ( 𝑗 ‘ 𝑧 ) )
85 73 80 84 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑗 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) ∧ 𝑧 ∈ 𝐼 ) → ( ( 𝑥 ‘ 𝑧 ) − ( ( 𝑥 ‘ 𝑧 ) − ( 𝑗 ‘ 𝑧 ) ) ) = ( 𝑗 ‘ 𝑧 ) )
86 85 mpteq2dva ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑗 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) → ( 𝑧 ∈ 𝐼 ↦ ( ( 𝑥 ‘ 𝑧 ) − ( ( 𝑥 ‘ 𝑧 ) − ( 𝑗 ‘ 𝑧 ) ) ) ) = ( 𝑧 ∈ 𝐼 ↦ ( 𝑗 ‘ 𝑧 ) ) )
87 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑗 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) → 𝐼 ∈ 𝑉 )
88 ovex ⊢ ( ( 𝑥 ‘ 𝑧 ) − ( 𝑗 ‘ 𝑧 ) ) ∈ V
89 88 a1i ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑗 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) ∧ 𝑧 ∈ 𝐼 ) → ( ( 𝑥 ‘ 𝑧 ) − ( 𝑗 ‘ 𝑧 ) ) ∈ V )
90 72 feqmptd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑗 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) → 𝑥 = ( 𝑧 ∈ 𝐼 ↦ ( 𝑥 ‘ 𝑧 ) ) )
91 79 feqmptd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑗 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) → 𝑗 = ( 𝑧 ∈ 𝐼 ↦ ( 𝑗 ‘ 𝑧 ) ) )
92 87 73 80 90 91 offval2 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑗 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) → ( 𝑥 ∘f − 𝑗 ) = ( 𝑧 ∈ 𝐼 ↦ ( ( 𝑥 ‘ 𝑧 ) − ( 𝑗 ‘ 𝑧 ) ) ) )
93 87 73 89 90 92 offval2 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑗 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) → ( 𝑥 ∘f − ( 𝑥 ∘f − 𝑗 ) ) = ( 𝑧 ∈ 𝐼 ↦ ( ( 𝑥 ‘ 𝑧 ) − ( ( 𝑥 ‘ 𝑧 ) − ( 𝑗 ‘ 𝑧 ) ) ) ) )
94 86 93 91 3eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑗 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) → ( 𝑥 ∘f − ( 𝑥 ∘f − 𝑗 ) ) = 𝑗 )
95 94 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑗 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) → ( 𝑌 ‘ ( 𝑥 ∘f − ( 𝑥 ∘f − 𝑗 ) ) ) = ( 𝑌 ‘ 𝑗 ) )
96 95 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑗 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) → ( ( 𝑋 ‘ ( 𝑥 ∘f − 𝑗 ) ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑥 ∘f − ( 𝑥 ∘f − 𝑗 ) ) ) ) = ( ( 𝑋 ‘ ( 𝑥 ∘f − 𝑗 ) ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ 𝑗 ) ) )
97 9 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑗 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) → 𝑅 ∈ CRing )
98 18 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑗 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) → 𝑋 : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
99 76 simprd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑗 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) → 𝑗 ∘r ≤ 𝑥 )
100 4 psrbagcon ⊢ ( ( 𝑥 ∈ 𝐷 ∧ 𝑗 : 𝐼 ⟶ ℕ0 ∧ 𝑗 ∘r ≤ 𝑥 ) → ( ( 𝑥 ∘f − 𝑗 ) ∈ 𝐷 ∧ ( 𝑥 ∘f − 𝑗 ) ∘r ≤ 𝑥 ) )
101 59 79 99 100 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑗 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) → ( ( 𝑥 ∘f − 𝑗 ) ∈ 𝐷 ∧ ( 𝑥 ∘f − 𝑗 ) ∘r ≤ 𝑥 ) )
102 101 simpld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑗 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) → ( 𝑥 ∘f − 𝑗 ) ∈ 𝐷 )
103 98 102 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑗 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) → ( 𝑋 ‘ ( 𝑥 ∘f − 𝑗 ) ) ∈ ( Base ‘ 𝑅 ) )
104 25 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑗 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) → 𝑌 : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
105 104 77 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑗 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) → ( 𝑌 ‘ 𝑗 ) ∈ ( Base ‘ 𝑅 ) )
106 10 35 crngcom ⊢ ( ( 𝑅 ∈ CRing ∧ ( 𝑋 ‘ ( 𝑥 ∘f − 𝑗 ) ) ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑌 ‘ 𝑗 ) ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝑋 ‘ ( 𝑥 ∘f − 𝑗 ) ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ 𝑗 ) ) = ( ( 𝑌 ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑋 ‘ ( 𝑥 ∘f − 𝑗 ) ) ) )
107 97 103 105 106 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑗 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) → ( ( 𝑋 ‘ ( 𝑥 ∘f − 𝑗 ) ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ 𝑗 ) ) = ( ( 𝑌 ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑋 ‘ ( 𝑥 ∘f − 𝑗 ) ) ) )
108 96 107 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑗 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ) → ( ( 𝑋 ‘ ( 𝑥 ∘f − 𝑗 ) ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑥 ∘f − ( 𝑥 ∘f − 𝑗 ) ) ) ) = ( ( 𝑌 ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑋 ‘ ( 𝑥 ∘f − 𝑗 ) ) ) )
109 108 mpteq2dva ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( 𝑗 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ↦ ( ( 𝑋 ‘ ( 𝑥 ∘f − 𝑗 ) ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑥 ∘f − ( 𝑥 ∘f − 𝑗 ) ) ) ) ) = ( 𝑗 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ↦ ( ( 𝑌 ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑋 ‘ ( 𝑥 ∘f − 𝑗 ) ) ) ) )
110 69 109 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( ( 𝑘 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ↦ ( ( 𝑋 ‘ 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑥 ∘f − 𝑘 ) ) ) ) ∘ ( 𝑗 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ↦ ( 𝑥 ∘f − 𝑗 ) ) ) = ( 𝑗 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ↦ ( ( 𝑌 ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑋 ‘ ( 𝑥 ∘f − 𝑗 ) ) ) ) )
111 110 oveq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( 𝑅 Σg ( ( 𝑘 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ↦ ( ( 𝑋 ‘ 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑥 ∘f − 𝑘 ) ) ) ) ∘ ( 𝑗 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ↦ ( 𝑥 ∘f − 𝑗 ) ) ) ) = ( 𝑅 Σg ( 𝑗 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ↦ ( ( 𝑌 ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑋 ‘ ( 𝑥 ∘f − 𝑗 ) ) ) ) ) )
112 58 111 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( 𝑅 Σg ( 𝑘 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ↦ ( ( 𝑋 ‘ 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑥 ∘f − 𝑘 ) ) ) ) ) = ( 𝑅 Σg ( 𝑗 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ↦ ( ( 𝑌 ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑋 ‘ ( 𝑥 ∘f − 𝑗 ) ) ) ) ) )
113 112 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑘 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ↦ ( ( 𝑋 ‘ 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑥 ∘f − 𝑘 ) ) ) ) ) ) = ( 𝑥 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑗 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ↦ ( ( 𝑌 ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑋 ‘ ( 𝑥 ∘f − 𝑗 ) ) ) ) ) ) )
114 1 6 35 5 4 7 8 psrmulfval ⊢ ( 𝜑 → ( 𝑋 × 𝑌 ) = ( 𝑥 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑘 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ↦ ( ( 𝑋 ‘ 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑥 ∘f − 𝑘 ) ) ) ) ) ) )
115 1 6 35 5 4 8 7 psrmulfval ⊢ ( 𝜑 → ( 𝑌 × 𝑋 ) = ( 𝑥 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑗 ∈ { 𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑥 } ↦ ( ( 𝑌 ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑋 ‘ ( 𝑥 ∘f − 𝑗 ) ) ) ) ) ) )
116 113 114 115 3eqtr4d ⊢ ( 𝜑 → ( 𝑋 × 𝑌 ) = ( 𝑌 × 𝑋 ) )