Metamath Proof Explorer


Theorem xpsvsca

Description: Value of the scalar multiplication function in a binary structure product. (Contributed by Mario Carneiro, 15-Aug-2015)

Ref Expression
Hypotheses xpssca.t T = R × 𝑠 S
xpssca.g G = Scalar R
xpssca.1 φ R V
xpssca.2 φ S W
xpsvsca.x X = Base R
xpsvsca.y Y = Base S
xpsvsca.k K = Base G
xpsvsca.m · ˙ = R
xpsvsca.n × ˙ = S
xpsvsca.p ˙ = T
xpsvsca.3 φ A K
xpsvsca.4 φ B X
xpsvsca.5 φ C Y
xpsvsca.6 φ A · ˙ B X
xpsvsca.7 φ A × ˙ C Y
Assertion xpsvsca φ A ˙ B C = A · ˙ B A × ˙ C

Proof

Step Hyp Ref Expression
1 xpssca.t T = R × 𝑠 S
2 xpssca.g G = Scalar R
3 xpssca.1 φ R V
4 xpssca.2 φ S W
5 xpsvsca.x X = Base R
6 xpsvsca.y Y = Base S
7 xpsvsca.k K = Base G
8 xpsvsca.m · ˙ = R
9 xpsvsca.n × ˙ = S
10 xpsvsca.p ˙ = T
11 xpsvsca.3 φ A K
12 xpsvsca.4 φ B X
13 xpsvsca.5 φ C Y
14 xpsvsca.6 φ A · ˙ B X
15 xpsvsca.7 φ A × ˙ C Y
16 df-ov B x X , y Y x 1 𝑜 y C = x X , y Y x 1 𝑜 y B C
17 eqid x X , y Y x 1 𝑜 y = x X , y Y x 1 𝑜 y
18 17 xpsfval B X C Y B x X , y Y x 1 𝑜 y C = B 1 𝑜 C
19 12 13 18 syl2anc φ B x X , y Y x 1 𝑜 y C = B 1 𝑜 C
20 16 19 eqtr3id φ x X , y Y x 1 𝑜 y B C = B 1 𝑜 C
21 12 13 opelxpd φ B C X × Y
22 17 xpsff1o2 x X , y Y x 1 𝑜 y : X × Y 1-1 onto ran x X , y Y x 1 𝑜 y
23 f1of x X , y Y x 1 𝑜 y : X × Y 1-1 onto ran x X , y Y x 1 𝑜 y x X , y Y x 1 𝑜 y : X × Y ran x X , y Y x 1 𝑜 y
24 22 23 ax-mp x X , y Y x 1 𝑜 y : X × Y ran x X , y Y x 1 𝑜 y
25 24 ffvelrni B C X × Y x X , y Y x 1 𝑜 y B C ran x X , y Y x 1 𝑜 y
26 21 25 syl φ x X , y Y x 1 𝑜 y B C ran x X , y Y x 1 𝑜 y
27 20 26 eqeltrrd φ B 1 𝑜 C ran x X , y Y x 1 𝑜 y
28 eqid G 𝑠 R 1 𝑜 S = G 𝑠 R 1 𝑜 S
29 1 5 6 3 4 17 2 28 xpsval φ T = x X , y Y x 1 𝑜 y -1 𝑠 G 𝑠 R 1 𝑜 S
30 1 5 6 3 4 17 2 28 xpsrnbas φ ran x X , y Y x 1 𝑜 y = Base G 𝑠 R 1 𝑜 S
31 f1ocnv x X , y Y x 1 𝑜 y : X × Y 1-1 onto ran x X , y Y x 1 𝑜 y x X , y Y x 1 𝑜 y -1 : ran x X , y Y x 1 𝑜 y 1-1 onto X × Y
32 22 31 mp1i φ x X , y Y x 1 𝑜 y -1 : ran x X , y Y x 1 𝑜 y 1-1 onto X × Y
33 f1ofo x X , y Y x 1 𝑜 y -1 : ran x X , y Y x 1 𝑜 y 1-1 onto X × Y x X , y Y x 1 𝑜 y -1 : ran x X , y Y x 1 𝑜 y onto X × Y
34 32 33 syl φ x X , y Y x 1 𝑜 y -1 : ran x X , y Y x 1 𝑜 y onto X × Y
35 ovexd φ G 𝑠 R 1 𝑜 S V
36 2 fvexi G V
37 36 a1i G V
38 prex R 1 𝑜 S V
39 38 a1i R 1 𝑜 S V
40 28 37 39 prdssca G = Scalar G 𝑠 R 1 𝑜 S
41 40 mptru G = Scalar G 𝑠 R 1 𝑜 S
42 eqid G 𝑠 R 1 𝑜 S = G 𝑠 R 1 𝑜 S
43 32 f1ovscpbl φ a K b ran x X , y Y x 1 𝑜 y c ran x X , y Y x 1 𝑜 y x X , y Y x 1 𝑜 y -1 b = x X , y Y x 1 𝑜 y -1 c x X , y Y x 1 𝑜 y -1 a G 𝑠 R 1 𝑜 S b = x X , y Y x 1 𝑜 y -1 a G 𝑠 R 1 𝑜 S c
44 29 30 34 35 41 7 42 10 43 imasvscaval φ A K B 1 𝑜 C ran x X , y Y x 1 𝑜 y A ˙ x X , y Y x 1 𝑜 y -1 B 1 𝑜 C = x X , y Y x 1 𝑜 y -1 A G 𝑠 R 1 𝑜 S B 1 𝑜 C
45 11 27 44 mpd3an23 φ A ˙ x X , y Y x 1 𝑜 y -1 B 1 𝑜 C = x X , y Y x 1 𝑜 y -1 A G 𝑠 R 1 𝑜 S B 1 𝑜 C
46 f1ocnvfv x X , y Y x 1 𝑜 y : X × Y 1-1 onto ran x X , y Y x 1 𝑜 y B C X × Y x X , y Y x 1 𝑜 y B C = B 1 𝑜 C x X , y Y x 1 𝑜 y -1 B 1 𝑜 C = B C
47 22 21 46 sylancr φ x X , y Y x 1 𝑜 y B C = B 1 𝑜 C x X , y Y x 1 𝑜 y -1 B 1 𝑜 C = B C
48 20 47 mpd φ x X , y Y x 1 𝑜 y -1 B 1 𝑜 C = B C
49 48 oveq2d φ A ˙ x X , y Y x 1 𝑜 y -1 B 1 𝑜 C = A ˙ B C
50 iftrue k = if k = R S = R
51 50 fveq2d k = if k = R S = R
52 51 8 eqtr4di k = if k = R S = · ˙
53 eqidd k = A = A
54 iftrue k = if k = B C = B
55 52 53 54 oveq123d k = A if k = R S if k = B C = A · ˙ B
56 iftrue k = if k = A · ˙ B A × ˙ C = A · ˙ B
57 55 56 eqtr4d k = A if k = R S if k = B C = if k = A · ˙ B A × ˙ C
58 iffalse ¬ k = if k = R S = S
59 58 fveq2d ¬ k = if k = R S = S
60 59 9 eqtr4di ¬ k = if k = R S = × ˙
61 eqidd ¬ k = A = A
62 iffalse ¬ k = if k = B C = C
63 60 61 62 oveq123d ¬ k = A if k = R S if k = B C = A × ˙ C
64 iffalse ¬ k = if k = A · ˙ B A × ˙ C = A × ˙ C
65 63 64 eqtr4d ¬ k = A if k = R S if k = B C = if k = A · ˙ B A × ˙ C
66 57 65 pm2.61i A if k = R S if k = B C = if k = A · ˙ B A × ˙ C
67 3 adantr φ k 2 𝑜 R V
68 4 adantr φ k 2 𝑜 S W
69 simpr φ k 2 𝑜 k 2 𝑜
70 fvprif R V S W k 2 𝑜 R 1 𝑜 S k = if k = R S
71 67 68 69 70 syl3anc φ k 2 𝑜 R 1 𝑜 S k = if k = R S
72 71 fveq2d φ k 2 𝑜 R 1 𝑜 S k = if k = R S
73 eqidd φ k 2 𝑜 A = A
74 12 adantr φ k 2 𝑜 B X
75 13 adantr φ k 2 𝑜 C Y
76 fvprif B X C Y k 2 𝑜 B 1 𝑜 C k = if k = B C
77 74 75 69 76 syl3anc φ k 2 𝑜 B 1 𝑜 C k = if k = B C
78 72 73 77 oveq123d φ k 2 𝑜 A R 1 𝑜 S k B 1 𝑜 C k = A if k = R S if k = B C
79 14 adantr φ k 2 𝑜 A · ˙ B X
80 15 adantr φ k 2 𝑜 A × ˙ C Y
81 fvprif A · ˙ B X A × ˙ C Y k 2 𝑜 A · ˙ B 1 𝑜 A × ˙ C k = if k = A · ˙ B A × ˙ C
82 79 80 69 81 syl3anc φ k 2 𝑜 A · ˙ B 1 𝑜 A × ˙ C k = if k = A · ˙ B A × ˙ C
83 66 78 82 3eqtr4a φ k 2 𝑜 A R 1 𝑜 S k B 1 𝑜 C k = A · ˙ B 1 𝑜 A × ˙ C k
84 83 mpteq2dva φ k 2 𝑜 A R 1 𝑜 S k B 1 𝑜 C k = k 2 𝑜 A · ˙ B 1 𝑜 A × ˙ C k
85 eqid Base G 𝑠 R 1 𝑜 S = Base G 𝑠 R 1 𝑜 S
86 36 a1i φ G V
87 2on 2 𝑜 On
88 87 a1i φ 2 𝑜 On
89 fnpr2o R V S W R 1 𝑜 S Fn 2 𝑜
90 3 4 89 syl2anc φ R 1 𝑜 S Fn 2 𝑜
91 27 30 eleqtrd φ B 1 𝑜 C Base G 𝑠 R 1 𝑜 S
92 28 85 42 7 86 88 90 11 91 prdsvscaval φ A G 𝑠 R 1 𝑜 S B 1 𝑜 C = k 2 𝑜 A R 1 𝑜 S k B 1 𝑜 C k
93 fnpr2o A · ˙ B X A × ˙ C Y A · ˙ B 1 𝑜 A × ˙ C Fn 2 𝑜
94 14 15 93 syl2anc φ A · ˙ B 1 𝑜 A × ˙ C Fn 2 𝑜
95 dffn5 A · ˙ B 1 𝑜 A × ˙ C Fn 2 𝑜 A · ˙ B 1 𝑜 A × ˙ C = k 2 𝑜 A · ˙ B 1 𝑜 A × ˙ C k
96 94 95 sylib φ A · ˙ B 1 𝑜 A × ˙ C = k 2 𝑜 A · ˙ B 1 𝑜 A × ˙ C k
97 84 92 96 3eqtr4d φ A G 𝑠 R 1 𝑜 S B 1 𝑜 C = A · ˙ B 1 𝑜 A × ˙ C
98 97 fveq2d φ x X , y Y x 1 𝑜 y -1 A G 𝑠 R 1 𝑜 S B 1 𝑜 C = x X , y Y x 1 𝑜 y -1 A · ˙ B 1 𝑜 A × ˙ C
99 df-ov A · ˙ B x X , y Y x 1 𝑜 y A × ˙ C = x X , y Y x 1 𝑜 y A · ˙ B A × ˙ C
100 17 xpsfval A · ˙ B X A × ˙ C Y A · ˙ B x X , y Y x 1 𝑜 y A × ˙ C = A · ˙ B 1 𝑜 A × ˙ C
101 14 15 100 syl2anc φ A · ˙ B x X , y Y x 1 𝑜 y A × ˙ C = A · ˙ B 1 𝑜 A × ˙ C
102 99 101 eqtr3id φ x X , y Y x 1 𝑜 y A · ˙ B A × ˙ C = A · ˙ B 1 𝑜 A × ˙ C
103 14 15 opelxpd φ A · ˙ B A × ˙ C X × Y
104 f1ocnvfv x X , y Y x 1 𝑜 y : X × Y 1-1 onto ran x X , y Y x 1 𝑜 y A · ˙ B A × ˙ C X × Y x X , y Y x 1 𝑜 y A · ˙ B A × ˙ C = A · ˙ B 1 𝑜 A × ˙ C x X , y Y x 1 𝑜 y -1 A · ˙ B 1 𝑜 A × ˙ C = A · ˙ B A × ˙ C
105 22 103 104 sylancr φ x X , y Y x 1 𝑜 y A · ˙ B A × ˙ C = A · ˙ B 1 𝑜 A × ˙ C x X , y Y x 1 𝑜 y -1 A · ˙ B 1 𝑜 A × ˙ C = A · ˙ B A × ˙ C
106 102 105 mpd φ x X , y Y x 1 𝑜 y -1 A · ˙ B 1 𝑜 A × ˙ C = A · ˙ B A × ˙ C
107 98 106 eqtrd φ x X , y Y x 1 𝑜 y -1 A G 𝑠 R 1 𝑜 S B 1 𝑜 C = A · ˙ B A × ˙ C
108 45 49 107 3eqtr3d φ A ˙ B C = A · ˙ B A × ˙ C