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