Metamath Proof Explorer


Theorem prdssca

Description: Scalar ring of a structure product. (Contributed by Stefan O'Rear, 5-Jan-2015) (Revised by Mario Carneiro, 15-Aug-2015) (Revised by Thierry Arnoux, 16-Jun-2019) (Revised by Zhi Wang, 18-Aug-2024)

Ref Expression
Hypotheses prdsbas.p P = S 𝑠 R
prdsbas.s φ S V
prdsbas.r φ R W
Assertion prdssca φ S = Scalar P

Proof

Step Hyp Ref Expression
1 prdsbas.p P = S 𝑠 R
2 prdsbas.s φ S V
3 prdsbas.r φ R W
4 eqid Base S = Base S
5 eqidd φ dom R = dom R
6 eqidd φ x dom R Base R x = x dom R Base R x
7 eqidd φ f x dom R Base R x , g x dom R Base R x x dom R f x + R x g x = f x dom R Base R x , g x dom R Base R x x dom R f x + R x g x
8 eqidd φ f x dom R Base R x , g x dom R Base R x x dom R f x R x g x = f x dom R Base R x , g x dom R Base R x x dom R f x R x g x
9 eqidd φ f Base S , g x dom R Base R x x dom R f R x g x = f Base S , g x dom R Base R x x dom R f R x g x
10 eqidd φ f x dom R Base R x , g x dom R Base R x S x dom R f x 𝑖 R x g x = f x dom R Base R x , g x dom R Base R x S x dom R f x 𝑖 R x g x
11 eqidd φ 𝑡 TopOpen R = 𝑡 TopOpen R
12 eqidd φ f g | f g x dom R Base R x x dom R f x R x g x = f g | f g x dom R Base R x x dom R f x R x g x
13 eqidd φ f x dom R Base R x , g x dom R Base R x sup ran x dom R f x dist R x g x 0 * < = f x dom R Base R x , g x dom R Base R x sup ran x dom R f x dist R x g x 0 * <
14 eqidd φ f x dom R Base R x , g x dom R Base R x x dom R f x Hom R x g x = f x dom R Base R x , g x dom R Base R x x dom R f x Hom R x g x
15 eqidd φ a x dom R Base R x × x dom R Base R x , c x dom R Base R x d 2 nd a f x dom R Base R x , g x dom R Base R x x dom R f x Hom R x g x c , e f x dom R Base R x , g x dom R Base R x x dom R f x Hom R x g x a x dom R d x 1 st a x 2 nd a x comp R x c x e x = a x dom R Base R x × x dom R Base R x , c x dom R Base R x d 2 nd a f x dom R Base R x , g x dom R Base R x x dom R f x Hom R x g x c , e f x dom R Base R x , g x dom R Base R x x dom R f x Hom R x g x a x dom R d x 1 st a x 2 nd a x comp R x c x e x
16 1 4 5 6 7 8 9 10 11 12 13 14 15 2 3 prdsval φ P = Base ndx x dom R Base R x + ndx f x dom R Base R x , g x dom R Base R x x dom R f x + R x g x ndx f x dom R Base R x , g x dom R Base R x x dom R f x R x g x Scalar ndx S ndx f Base S , g x dom R Base R x x dom R f R x g x 𝑖 ndx f x dom R Base R x , g x dom R Base R x S x dom R f x 𝑖 R x g x TopSet ndx 𝑡 TopOpen R ndx f g | f g x dom R Base R x x dom R f x R x g x dist ndx f x dom R Base R x , g x dom R Base R x sup ran x dom R f x dist R x g x 0 * < Hom ndx f x dom R Base R x , g x dom R Base R x x dom R f x Hom R x g x comp ndx a x dom R Base R x × x dom R Base R x , c x dom R Base R x d 2 nd a f x dom R Base R x , g x dom R Base R x x dom R f x Hom R x g x c , e f x dom R Base R x , g x dom R Base R x x dom R f x Hom R x g x a x dom R d x 1 st a x 2 nd a x comp R x c x e x
17 eqid Scalar P = Scalar P
18 scaid Scalar = Slot Scalar ndx
19 snsstp1 Scalar ndx S Scalar ndx S ndx f Base S , g x dom R Base R x x dom R f R x g x 𝑖 ndx f x dom R Base R x , g x dom R Base R x S x dom R f x 𝑖 R x g x
20 ssun2 Scalar ndx S ndx f Base S , g x dom R Base R x x dom R f R x g x 𝑖 ndx f x dom R Base R x , g x dom R Base R x S x dom R f x 𝑖 R x g x Base ndx x dom R Base R x + ndx f x dom R Base R x , g x dom R Base R x x dom R f x + R x g x ndx f x dom R Base R x , g x dom R Base R x x dom R f x R x g x Scalar ndx S ndx f Base S , g x dom R Base R x x dom R f R x g x 𝑖 ndx f x dom R Base R x , g x dom R Base R x S x dom R f x 𝑖 R x g x
21 19 20 sstri Scalar ndx S Base ndx x dom R Base R x + ndx f x dom R Base R x , g x dom R Base R x x dom R f x + R x g x ndx f x dom R Base R x , g x dom R Base R x x dom R f x R x g x Scalar ndx S ndx f Base S , g x dom R Base R x x dom R f R x g x 𝑖 ndx f x dom R Base R x , g x dom R Base R x S x dom R f x 𝑖 R x g x
22 ssun1 Base ndx x dom R Base R x + ndx f x dom R Base R x , g x dom R Base R x x dom R f x + R x g x ndx f x dom R Base R x , g x dom R Base R x x dom R f x R x g x Scalar ndx S ndx f Base S , g x dom R Base R x x dom R f R x g x 𝑖 ndx f x dom R Base R x , g x dom R Base R x S x dom R f x 𝑖 R x g x Base ndx x dom R Base R x + ndx f x dom R Base R x , g x dom R Base R x x dom R f x + R x g x ndx f x dom R Base R x , g x dom R Base R x x dom R f x R x g x Scalar ndx S ndx f Base S , g x dom R Base R x x dom R f R x g x 𝑖 ndx f x dom R Base R x , g x dom R Base R x S x dom R f x 𝑖 R x g x TopSet ndx 𝑡 TopOpen R ndx f g | f g x dom R Base R x x dom R f x R x g x dist ndx f x dom R Base R x , g x dom R Base R x sup ran x dom R f x dist R x g x 0 * < Hom ndx f x dom R Base R x , g x dom R Base R x x dom R f x Hom R x g x comp ndx a x dom R Base R x × x dom R Base R x , c x dom R Base R x d 2 nd a f x dom R Base R x , g x dom R Base R x x dom R f x Hom R x g x c , e f x dom R Base R x , g x dom R Base R x x dom R f x Hom R x g x a x dom R d x 1 st a x 2 nd a x comp R x c x e x
23 21 22 sstri Scalar ndx S Base ndx x dom R Base R x + ndx f x dom R Base R x , g x dom R Base R x x dom R f x + R x g x ndx f x dom R Base R x , g x dom R Base R x x dom R f x R x g x Scalar ndx S ndx f Base S , g x dom R Base R x x dom R f R x g x 𝑖 ndx f x dom R Base R x , g x dom R Base R x S x dom R f x 𝑖 R x g x TopSet ndx 𝑡 TopOpen R ndx f g | f g x dom R Base R x x dom R f x R x g x dist ndx f x dom R Base R x , g x dom R Base R x sup ran x dom R f x dist R x g x 0 * < Hom ndx f x dom R Base R x , g x dom R Base R x x dom R f x Hom R x g x comp ndx a x dom R Base R x × x dom R Base R x , c x dom R Base R x d 2 nd a f x dom R Base R x , g x dom R Base R x x dom R f x Hom R x g x c , e f x dom R Base R x , g x dom R Base R x x dom R f x Hom R x g x a x dom R d x 1 st a x 2 nd a x comp R x c x e x
24 16 17 18 2 23 prdsbaslem φ Scalar P = S
25 24 eqcomd φ S = Scalar P