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