Metamath Proof Explorer


Theorem psrass23

Description: Associative identities for the ring of power series. (Contributed by Mario Carneiro, 7-Jan-2015) (Proof shortened by AV, 25-Nov-2019)

Ref Expression
Hypotheses psrring.s S = I mPwSer R
psrring.i φ I V
psrring.r φ R Ring
psrass.d D = f 0 I | f -1 Fin
psrass.t × ˙ = S
psrass.b B = Base S
psrass.x φ X B
psrass.y φ Y B
psrcom.c φ R CRing
psrass.k K = Base R
psrass.n · ˙ = S
psrass.a φ A K
Assertion psrass23 φ A · ˙ X × ˙ Y = A · ˙ X × ˙ Y X × ˙ A · ˙ Y = A · ˙ X × ˙ Y

Proof

Step Hyp Ref Expression
1 psrring.s S = I mPwSer R
2 psrring.i φ I V
3 psrring.r φ R Ring
4 psrass.d D = f 0 I | f -1 Fin
5 psrass.t × ˙ = S
6 psrass.b B = Base S
7 psrass.x φ X B
8 psrass.y φ Y B
9 psrcom.c φ R CRing
10 psrass.k K = Base R
11 psrass.n · ˙ = S
12 psrass.a φ A K
13 1 2 3 4 5 6 7 8 10 11 12 psrass23l φ A · ˙ X × ˙ Y = A · ˙ X × ˙ Y
14 eqid Base R = Base R
15 eqid R = R
16 12 adantr φ k D A K
17 16 10 eleqtrdi φ k D A Base R
18 17 adantr φ k D x y D | y f k A Base R
19 8 ad2antrr φ k D x y D | y f k Y B
20 ssrab2 y D | y f k D
21 simplr φ k D x y D | y f k k D
22 simpr φ k D x y D | y f k x y D | y f k
23 eqid y D | y f k = y D | y f k
24 4 23 psrbagconcl k D x y D | y f k k f x y D | y f k
25 21 22 24 syl2anc φ k D x y D | y f k k f x y D | y f k
26 20 25 sseldi φ k D x y D | y f k k f x D
27 1 11 14 6 15 4 18 19 26 psrvscaval φ k D x y D | y f k A · ˙ Y k f x = A R Y k f x
28 27 oveq2d φ k D x y D | y f k X x R A · ˙ Y k f x = X x R A R Y k f x
29 7 ad2antrr φ k D x y D | y f k X B
30 1 14 4 6 29 psrelbas φ k D x y D | y f k X : D Base R
31 20 22 sseldi φ k D x y D | y f k x D
32 30 31 ffvelrnd φ k D x y D | y f k X x Base R
33 1 14 4 6 19 psrelbas φ k D x y D | y f k Y : D Base R
34 33 26 ffvelrnd φ k D x y D | y f k Y k f x Base R
35 9 ad2antrr φ k D x y D | y f k R CRing
36 14 15 crngcom R CRing u Base R v Base R u R v = v R u
37 36 3expb R CRing u Base R v Base R u R v = v R u
38 35 37 sylan φ k D x y D | y f k u Base R v Base R u R v = v R u
39 3 ad2antrr φ k D x y D | y f k R Ring
40 14 15 ringass R Ring u Base R v Base R w Base R u R v R w = u R v R w
41 39 40 sylan φ k D x y D | y f k u Base R v Base R w Base R u R v R w = u R v R w
42 32 18 34 38 41 caov12d φ k D x y D | y f k X x R A R Y k f x = A R X x R Y k f x
43 28 42 eqtrd φ k D x y D | y f k X x R A · ˙ Y k f x = A R X x R Y k f x
44 43 mpteq2dva φ k D x y D | y f k X x R A · ˙ Y k f x = x y D | y f k A R X x R Y k f x
45 44 oveq2d φ k D R x y D | y f k X x R A · ˙ Y k f x = R x y D | y f k A R X x R Y k f x
46 eqid 0 R = 0 R
47 eqid + R = + R
48 3 adantr φ k D R Ring
49 4 psrbaglefi k D y D | y f k Fin
50 49 adantl φ k D y D | y f k Fin
51 14 15 ringcl R Ring X x Base R Y k f x Base R X x R Y k f x Base R
52 39 32 34 51 syl3anc φ k D x y D | y f k X x R Y k f x Base R
53 ovex 0 I V
54 4 53 rabex2 D V
55 54 mptrabex x y D | y f k X x R Y k f x V
56 funmpt Fun x y D | y f k X x R Y k f x
57 fvex 0 R V
58 55 56 57 3pm3.2i x y D | y f k X x R Y k f x V Fun x y D | y f k X x R Y k f x 0 R V
59 58 a1i φ k D x y D | y f k X x R Y k f x V Fun x y D | y f k X x R Y k f x 0 R V
60 suppssdm x y D | y f k X x R Y k f x supp 0 R dom x y D | y f k X x R Y k f x
61 eqid x y D | y f k X x R Y k f x = x y D | y f k X x R Y k f x
62 61 dmmptss dom x y D | y f k X x R Y k f x y D | y f k
63 60 62 sstri x y D | y f k X x R Y k f x supp 0 R y D | y f k
64 63 a1i φ k D x y D | y f k X x R Y k f x supp 0 R y D | y f k
65 suppssfifsupp x y D | y f k X x R Y k f x V Fun x y D | y f k X x R Y k f x 0 R V y D | y f k Fin x y D | y f k X x R Y k f x supp 0 R y D | y f k finSupp 0 R x y D | y f k X x R Y k f x
66 59 50 64 65 syl12anc φ k D finSupp 0 R x y D | y f k X x R Y k f x
67 14 46 47 15 48 50 17 52 66 gsummulc2 φ k D R x y D | y f k A R X x R Y k f x = A R R x y D | y f k X x R Y k f x
68 45 67 eqtrd φ k D R x y D | y f k X x R A · ˙ Y k f x = A R R x y D | y f k X x R Y k f x
69 68 mpteq2dva φ k D R x y D | y f k X x R A · ˙ Y k f x = k D A R R x y D | y f k X x R Y k f x
70 1 11 10 6 3 12 8 psrvscacl φ A · ˙ Y B
71 1 6 15 5 4 7 70 psrmulfval φ X × ˙ A · ˙ Y = k D R x y D | y f k X x R A · ˙ Y k f x
72 1 6 5 3 7 8 psrmulcl φ X × ˙ Y B
73 1 11 10 6 15 4 12 72 psrvsca φ A · ˙ X × ˙ Y = D × A R f X × ˙ Y
74 54 a1i φ D V
75 ovex R x y D | y f k X x R Y k f x V
76 75 a1i φ k D R x y D | y f k X x R Y k f x V
77 fconstmpt D × A = k D A
78 77 a1i φ D × A = k D A
79 1 6 15 5 4 7 8 psrmulfval φ X × ˙ Y = k D R x y D | y f k X x R Y k f x
80 74 16 76 78 79 offval2 φ D × A R f X × ˙ Y = k D A R R x y D | y f k X x R Y k f x
81 73 80 eqtrd φ A · ˙ X × ˙ Y = k D A R R x y D | y f k X x R Y k f x
82 69 71 81 3eqtr4d φ X × ˙ A · ˙ Y = A · ˙ X × ˙ Y
83 13 82 jca φ A · ˙ X × ˙ Y = A · ˙ X × ˙ Y X × ˙ A · ˙ Y = A · ˙ X × ˙ Y