Metamath Proof Explorer


Theorem xpsrnbas

Description: The indexed structure product that appears in xpsval has the same base as the target of the function F . (Contributed by Mario Carneiro, 15-Aug-2015) (Revised by Jim Kingdon, 25-Sep-2023)

Ref Expression
Hypotheses xpsval.t T = R × 𝑠 S
xpsval.x X = Base R
xpsval.y Y = Base S
xpsval.1 φ R V
xpsval.2 φ S W
xpsval.f F = x X , y Y x 1 𝑜 y
xpsval.k G = Scalar R
xpsval.u U = G 𝑠 R 1 𝑜 S
Assertion xpsrnbas φ ran F = Base U

Proof

Step Hyp Ref Expression
1 xpsval.t T = R × 𝑠 S
2 xpsval.x X = Base R
3 xpsval.y Y = Base S
4 xpsval.1 φ R V
5 xpsval.2 φ S W
6 xpsval.f F = x X , y Y x 1 𝑜 y
7 xpsval.k G = Scalar R
8 xpsval.u U = G 𝑠 R 1 𝑜 S
9 eqid Base U = Base U
10 7 fvexi G V
11 10 a1i φ G V
12 2on 2 𝑜 On
13 12 a1i φ 2 𝑜 On
14 fnpr2o R V S W R 1 𝑜 S Fn 2 𝑜
15 4 5 14 syl2anc φ R 1 𝑜 S Fn 2 𝑜
16 8 9 11 13 15 prdsbas2 φ Base U = k 2 𝑜 Base R 1 𝑜 S k
17 fvprif R V S W k 2 𝑜 R 1 𝑜 S k = if k = R S
18 17 3expia R V S W k 2 𝑜 R 1 𝑜 S k = if k = R S
19 4 5 18 syl2anc φ k 2 𝑜 R 1 𝑜 S k = if k = R S
20 19 imp φ k 2 𝑜 R 1 𝑜 S k = if k = R S
21 20 fveq2d φ k 2 𝑜 Base R 1 𝑜 S k = Base if k = R S
22 ifeq12 X = Base R Y = Base S if k = X Y = if k = Base R Base S
23 2 3 22 mp2an if k = X Y = if k = Base R Base S
24 fvif Base if k = R S = if k = Base R Base S
25 23 24 eqtr4i if k = X Y = Base if k = R S
26 21 25 eqtr4di φ k 2 𝑜 Base R 1 𝑜 S k = if k = X Y
27 26 ixpeq2dva φ k 2 𝑜 Base R 1 𝑜 S k = k 2 𝑜 if k = X Y
28 6 xpsfrn ran F = k 2 𝑜 if k = X Y
29 27 28 eqtr4di φ k 2 𝑜 Base R 1 𝑜 S k = ran F
30 16 29 eqtr2d φ ran F = Base U