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 𝑇 = ( 𝑅 ×s 𝑆 )
xpssca.g 𝐺 = ( Scalar ‘ 𝑅 )
xpssca.1 ( 𝜑𝑅𝑉 )
xpssca.2 ( 𝜑𝑆𝑊 )
xpsvsca.x 𝑋 = ( Base ‘ 𝑅 )
xpsvsca.y 𝑌 = ( Base ‘ 𝑆 )
xpsvsca.k 𝐾 = ( Base ‘ 𝐺 )
xpsvsca.m · = ( ·𝑠𝑅 )
xpsvsca.n × = ( ·𝑠𝑆 )
xpsvsca.p = ( ·𝑠𝑇 )
xpsvsca.3 ( 𝜑𝐴𝐾 )
xpsvsca.4 ( 𝜑𝐵𝑋 )
xpsvsca.5 ( 𝜑𝐶𝑌 )
xpsvsca.6 ( 𝜑 → ( 𝐴 · 𝐵 ) ∈ 𝑋 )
xpsvsca.7 ( 𝜑 → ( 𝐴 × 𝐶 ) ∈ 𝑌 )
Assertion xpsvsca ( 𝜑 → ( 𝐴 𝐵 , 𝐶 ⟩ ) = ⟨ ( 𝐴 · 𝐵 ) , ( 𝐴 × 𝐶 ) ⟩ )

Proof

Step Hyp Ref Expression
1 xpssca.t 𝑇 = ( 𝑅 ×s 𝑆 )
2 xpssca.g 𝐺 = ( Scalar ‘ 𝑅 )
3 xpssca.1 ( 𝜑𝑅𝑉 )
4 xpssca.2 ( 𝜑𝑆𝑊 )
5 xpsvsca.x 𝑋 = ( Base ‘ 𝑅 )
6 xpsvsca.y 𝑌 = ( Base ‘ 𝑆 )
7 xpsvsca.k 𝐾 = ( Base ‘ 𝐺 )
8 xpsvsca.m · = ( ·𝑠𝑅 )
9 xpsvsca.n × = ( ·𝑠𝑆 )
10 xpsvsca.p = ( ·𝑠𝑇 )
11 xpsvsca.3 ( 𝜑𝐴𝐾 )
12 xpsvsca.4 ( 𝜑𝐵𝑋 )
13 xpsvsca.5 ( 𝜑𝐶𝑌 )
14 xpsvsca.6 ( 𝜑 → ( 𝐴 · 𝐵 ) ∈ 𝑋 )
15 xpsvsca.7 ( 𝜑 → ( 𝐴 × 𝐶 ) ∈ 𝑌 )
16 df-ov ( 𝐵 ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) 𝐶 ) = ( ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ‘ ⟨ 𝐵 , 𝐶 ⟩ )
17 eqid ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) = ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } )
18 17 xpsfval ( ( 𝐵𝑋𝐶𝑌 ) → ( 𝐵 ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) 𝐶 ) = { ⟨ ∅ , 𝐵 ⟩ , ⟨ 1o , 𝐶 ⟩ } )
19 12 13 18 syl2anc ( 𝜑 → ( 𝐵 ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) 𝐶 ) = { ⟨ ∅ , 𝐵 ⟩ , ⟨ 1o , 𝐶 ⟩ } )
20 16 19 eqtr3id ( 𝜑 → ( ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ‘ ⟨ 𝐵 , 𝐶 ⟩ ) = { ⟨ ∅ , 𝐵 ⟩ , ⟨ 1o , 𝐶 ⟩ } )
21 12 13 opelxpd ( 𝜑 → ⟨ 𝐵 , 𝐶 ⟩ ∈ ( 𝑋 × 𝑌 ) )
22 17 xpsff1o2 ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) : ( 𝑋 × 𝑌 ) –1-1-onto→ ran ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } )
23 f1of ( ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) : ( 𝑋 × 𝑌 ) –1-1-onto→ ran ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) → ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) : ( 𝑋 × 𝑌 ) ⟶ ran ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) )
24 22 23 ax-mp ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) : ( 𝑋 × 𝑌 ) ⟶ ran ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } )
25 24 ffvelrni ( ⟨ 𝐵 , 𝐶 ⟩ ∈ ( 𝑋 × 𝑌 ) → ( ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ‘ ⟨ 𝐵 , 𝐶 ⟩ ) ∈ ran ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) )
26 21 25 syl ( 𝜑 → ( ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ‘ ⟨ 𝐵 , 𝐶 ⟩ ) ∈ ran ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) )
27 20 26 eqeltrrd ( 𝜑 → { ⟨ ∅ , 𝐵 ⟩ , ⟨ 1o , 𝐶 ⟩ } ∈ ran ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) )
28 eqid ( 𝐺 Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) = ( 𝐺 Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } )
29 1 5 6 3 4 17 2 28 xpsval ( 𝜑𝑇 = ( ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) “s ( 𝐺 Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ) )
30 1 5 6 3 4 17 2 28 xpsrnbas ( 𝜑 → ran ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) = ( Base ‘ ( 𝐺 Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ) )
31 f1ocnv ( ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) : ( 𝑋 × 𝑌 ) –1-1-onto→ ran ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) → ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) : ran ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) –1-1-onto→ ( 𝑋 × 𝑌 ) )
32 22 31 mp1i ( 𝜑 ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) : ran ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) –1-1-onto→ ( 𝑋 × 𝑌 ) )
33 f1ofo ( ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) : ran ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) –1-1-onto→ ( 𝑋 × 𝑌 ) → ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) : ran ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) –onto→ ( 𝑋 × 𝑌 ) )
34 32 33 syl ( 𝜑 ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) : ran ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) –onto→ ( 𝑋 × 𝑌 ) )
35 ovexd ( 𝜑 → ( 𝐺 Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ∈ V )
36 2 fvexi 𝐺 ∈ V
37 36 a1i ( ⊤ → 𝐺 ∈ V )
38 prex { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ∈ V
39 38 a1i ( ⊤ → { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ∈ V )
40 28 37 39 prdssca ( ⊤ → 𝐺 = ( Scalar ‘ ( 𝐺 Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ) )
41 40 mptru 𝐺 = ( Scalar ‘ ( 𝐺 Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) )
42 eqid ( ·𝑠 ‘ ( 𝐺 Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ) = ( ·𝑠 ‘ ( 𝐺 Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) )
43 32 f1ovscpbl ( ( 𝜑 ∧ ( 𝑎𝐾𝑏 ∈ ran ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ∧ 𝑐 ∈ ran ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ) ) → ( ( ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ‘ 𝑏 ) = ( ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ‘ 𝑐 ) → ( ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ‘ ( 𝑎 ( ·𝑠 ‘ ( 𝐺 Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ) 𝑏 ) ) = ( ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ‘ ( 𝑎 ( ·𝑠 ‘ ( 𝐺 Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ) 𝑐 ) ) ) )
44 29 30 34 35 41 7 42 10 43 imasvscaval ( ( 𝜑𝐴𝐾 ∧ { ⟨ ∅ , 𝐵 ⟩ , ⟨ 1o , 𝐶 ⟩ } ∈ ran ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ) → ( 𝐴 ( ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ‘ { ⟨ ∅ , 𝐵 ⟩ , ⟨ 1o , 𝐶 ⟩ } ) ) = ( ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ‘ ( 𝐴 ( ·𝑠 ‘ ( 𝐺 Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ) { ⟨ ∅ , 𝐵 ⟩ , ⟨ 1o , 𝐶 ⟩ } ) ) )
45 11 27 44 mpd3an23 ( 𝜑 → ( 𝐴 ( ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ‘ { ⟨ ∅ , 𝐵 ⟩ , ⟨ 1o , 𝐶 ⟩ } ) ) = ( ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ‘ ( 𝐴 ( ·𝑠 ‘ ( 𝐺 Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ) { ⟨ ∅ , 𝐵 ⟩ , ⟨ 1o , 𝐶 ⟩ } ) ) )
46 f1ocnvfv ( ( ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) : ( 𝑋 × 𝑌 ) –1-1-onto→ ran ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ∧ ⟨ 𝐵 , 𝐶 ⟩ ∈ ( 𝑋 × 𝑌 ) ) → ( ( ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ‘ ⟨ 𝐵 , 𝐶 ⟩ ) = { ⟨ ∅ , 𝐵 ⟩ , ⟨ 1o , 𝐶 ⟩ } → ( ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ‘ { ⟨ ∅ , 𝐵 ⟩ , ⟨ 1o , 𝐶 ⟩ } ) = ⟨ 𝐵 , 𝐶 ⟩ ) )
47 22 21 46 sylancr ( 𝜑 → ( ( ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ‘ ⟨ 𝐵 , 𝐶 ⟩ ) = { ⟨ ∅ , 𝐵 ⟩ , ⟨ 1o , 𝐶 ⟩ } → ( ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ‘ { ⟨ ∅ , 𝐵 ⟩ , ⟨ 1o , 𝐶 ⟩ } ) = ⟨ 𝐵 , 𝐶 ⟩ ) )
48 20 47 mpd ( 𝜑 → ( ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ‘ { ⟨ ∅ , 𝐵 ⟩ , ⟨ 1o , 𝐶 ⟩ } ) = ⟨ 𝐵 , 𝐶 ⟩ )
49 48 oveq2d ( 𝜑 → ( 𝐴 ( ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ‘ { ⟨ ∅ , 𝐵 ⟩ , ⟨ 1o , 𝐶 ⟩ } ) ) = ( 𝐴 𝐵 , 𝐶 ⟩ ) )
50 iftrue ( 𝑘 = ∅ → if ( 𝑘 = ∅ , 𝑅 , 𝑆 ) = 𝑅 )
51 50 fveq2d ( 𝑘 = ∅ → ( ·𝑠 ‘ if ( 𝑘 = ∅ , 𝑅 , 𝑆 ) ) = ( ·𝑠𝑅 ) )
52 51 8 eqtr4di ( 𝑘 = ∅ → ( ·𝑠 ‘ if ( 𝑘 = ∅ , 𝑅 , 𝑆 ) ) = · )
53 eqidd ( 𝑘 = ∅ → 𝐴 = 𝐴 )
54 iftrue ( 𝑘 = ∅ → if ( 𝑘 = ∅ , 𝐵 , 𝐶 ) = 𝐵 )
55 52 53 54 oveq123d ( 𝑘 = ∅ → ( 𝐴 ( ·𝑠 ‘ if ( 𝑘 = ∅ , 𝑅 , 𝑆 ) ) if ( 𝑘 = ∅ , 𝐵 , 𝐶 ) ) = ( 𝐴 · 𝐵 ) )
56 iftrue ( 𝑘 = ∅ → if ( 𝑘 = ∅ , ( 𝐴 · 𝐵 ) , ( 𝐴 × 𝐶 ) ) = ( 𝐴 · 𝐵 ) )
57 55 56 eqtr4d ( 𝑘 = ∅ → ( 𝐴 ( ·𝑠 ‘ if ( 𝑘 = ∅ , 𝑅 , 𝑆 ) ) if ( 𝑘 = ∅ , 𝐵 , 𝐶 ) ) = if ( 𝑘 = ∅ , ( 𝐴 · 𝐵 ) , ( 𝐴 × 𝐶 ) ) )
58 iffalse ( ¬ 𝑘 = ∅ → if ( 𝑘 = ∅ , 𝑅 , 𝑆 ) = 𝑆 )
59 58 fveq2d ( ¬ 𝑘 = ∅ → ( ·𝑠 ‘ if ( 𝑘 = ∅ , 𝑅 , 𝑆 ) ) = ( ·𝑠𝑆 ) )
60 59 9 eqtr4di ( ¬ 𝑘 = ∅ → ( ·𝑠 ‘ if ( 𝑘 = ∅ , 𝑅 , 𝑆 ) ) = × )
61 eqidd ( ¬ 𝑘 = ∅ → 𝐴 = 𝐴 )
62 iffalse ( ¬ 𝑘 = ∅ → if ( 𝑘 = ∅ , 𝐵 , 𝐶 ) = 𝐶 )
63 60 61 62 oveq123d ( ¬ 𝑘 = ∅ → ( 𝐴 ( ·𝑠 ‘ if ( 𝑘 = ∅ , 𝑅 , 𝑆 ) ) if ( 𝑘 = ∅ , 𝐵 , 𝐶 ) ) = ( 𝐴 × 𝐶 ) )
64 iffalse ( ¬ 𝑘 = ∅ → if ( 𝑘 = ∅ , ( 𝐴 · 𝐵 ) , ( 𝐴 × 𝐶 ) ) = ( 𝐴 × 𝐶 ) )
65 63 64 eqtr4d ( ¬ 𝑘 = ∅ → ( 𝐴 ( ·𝑠 ‘ if ( 𝑘 = ∅ , 𝑅 , 𝑆 ) ) if ( 𝑘 = ∅ , 𝐵 , 𝐶 ) ) = if ( 𝑘 = ∅ , ( 𝐴 · 𝐵 ) , ( 𝐴 × 𝐶 ) ) )
66 57 65 pm2.61i ( 𝐴 ( ·𝑠 ‘ if ( 𝑘 = ∅ , 𝑅 , 𝑆 ) ) if ( 𝑘 = ∅ , 𝐵 , 𝐶 ) ) = if ( 𝑘 = ∅ , ( 𝐴 · 𝐵 ) , ( 𝐴 × 𝐶 ) )
67 3 adantr ( ( 𝜑𝑘 ∈ 2o ) → 𝑅𝑉 )
68 4 adantr ( ( 𝜑𝑘 ∈ 2o ) → 𝑆𝑊 )
69 simpr ( ( 𝜑𝑘 ∈ 2o ) → 𝑘 ∈ 2o )
70 fvprif ( ( 𝑅𝑉𝑆𝑊𝑘 ∈ 2o ) → ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) = if ( 𝑘 = ∅ , 𝑅 , 𝑆 ) )
71 67 68 69 70 syl3anc ( ( 𝜑𝑘 ∈ 2o ) → ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) = if ( 𝑘 = ∅ , 𝑅 , 𝑆 ) )
72 71 fveq2d ( ( 𝜑𝑘 ∈ 2o ) → ( ·𝑠 ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) = ( ·𝑠 ‘ if ( 𝑘 = ∅ , 𝑅 , 𝑆 ) ) )
73 eqidd ( ( 𝜑𝑘 ∈ 2o ) → 𝐴 = 𝐴 )
74 12 adantr ( ( 𝜑𝑘 ∈ 2o ) → 𝐵𝑋 )
75 13 adantr ( ( 𝜑𝑘 ∈ 2o ) → 𝐶𝑌 )
76 fvprif ( ( 𝐵𝑋𝐶𝑌𝑘 ∈ 2o ) → ( { ⟨ ∅ , 𝐵 ⟩ , ⟨ 1o , 𝐶 ⟩ } ‘ 𝑘 ) = if ( 𝑘 = ∅ , 𝐵 , 𝐶 ) )
77 74 75 69 76 syl3anc ( ( 𝜑𝑘 ∈ 2o ) → ( { ⟨ ∅ , 𝐵 ⟩ , ⟨ 1o , 𝐶 ⟩ } ‘ 𝑘 ) = if ( 𝑘 = ∅ , 𝐵 , 𝐶 ) )
78 72 73 77 oveq123d ( ( 𝜑𝑘 ∈ 2o ) → ( 𝐴 ( ·𝑠 ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) ( { ⟨ ∅ , 𝐵 ⟩ , ⟨ 1o , 𝐶 ⟩ } ‘ 𝑘 ) ) = ( 𝐴 ( ·𝑠 ‘ if ( 𝑘 = ∅ , 𝑅 , 𝑆 ) ) if ( 𝑘 = ∅ , 𝐵 , 𝐶 ) ) )
79 14 adantr ( ( 𝜑𝑘 ∈ 2o ) → ( 𝐴 · 𝐵 ) ∈ 𝑋 )
80 15 adantr ( ( 𝜑𝑘 ∈ 2o ) → ( 𝐴 × 𝐶 ) ∈ 𝑌 )
81 fvprif ( ( ( 𝐴 · 𝐵 ) ∈ 𝑋 ∧ ( 𝐴 × 𝐶 ) ∈ 𝑌𝑘 ∈ 2o ) → ( { ⟨ ∅ , ( 𝐴 · 𝐵 ) ⟩ , ⟨ 1o , ( 𝐴 × 𝐶 ) ⟩ } ‘ 𝑘 ) = if ( 𝑘 = ∅ , ( 𝐴 · 𝐵 ) , ( 𝐴 × 𝐶 ) ) )
82 79 80 69 81 syl3anc ( ( 𝜑𝑘 ∈ 2o ) → ( { ⟨ ∅ , ( 𝐴 · 𝐵 ) ⟩ , ⟨ 1o , ( 𝐴 × 𝐶 ) ⟩ } ‘ 𝑘 ) = if ( 𝑘 = ∅ , ( 𝐴 · 𝐵 ) , ( 𝐴 × 𝐶 ) ) )
83 66 78 82 3eqtr4a ( ( 𝜑𝑘 ∈ 2o ) → ( 𝐴 ( ·𝑠 ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) ( { ⟨ ∅ , 𝐵 ⟩ , ⟨ 1o , 𝐶 ⟩ } ‘ 𝑘 ) ) = ( { ⟨ ∅ , ( 𝐴 · 𝐵 ) ⟩ , ⟨ 1o , ( 𝐴 × 𝐶 ) ⟩ } ‘ 𝑘 ) )
84 83 mpteq2dva ( 𝜑 → ( 𝑘 ∈ 2o ↦ ( 𝐴 ( ·𝑠 ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) ( { ⟨ ∅ , 𝐵 ⟩ , ⟨ 1o , 𝐶 ⟩ } ‘ 𝑘 ) ) ) = ( 𝑘 ∈ 2o ↦ ( { ⟨ ∅ , ( 𝐴 · 𝐵 ) ⟩ , ⟨ 1o , ( 𝐴 × 𝐶 ) ⟩ } ‘ 𝑘 ) ) )
85 eqid ( Base ‘ ( 𝐺 Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ) = ( Base ‘ ( 𝐺 Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) )
86 36 a1i ( 𝜑𝐺 ∈ V )
87 2on 2o ∈ On
88 87 a1i ( 𝜑 → 2o ∈ On )
89 fnpr2o ( ( 𝑅𝑉𝑆𝑊 ) → { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } Fn 2o )
90 3 4 89 syl2anc ( 𝜑 → { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } Fn 2o )
91 27 30 eleqtrd ( 𝜑 → { ⟨ ∅ , 𝐵 ⟩ , ⟨ 1o , 𝐶 ⟩ } ∈ ( Base ‘ ( 𝐺 Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ) )
92 28 85 42 7 86 88 90 11 91 prdsvscaval ( 𝜑 → ( 𝐴 ( ·𝑠 ‘ ( 𝐺 Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ) { ⟨ ∅ , 𝐵 ⟩ , ⟨ 1o , 𝐶 ⟩ } ) = ( 𝑘 ∈ 2o ↦ ( 𝐴 ( ·𝑠 ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) ( { ⟨ ∅ , 𝐵 ⟩ , ⟨ 1o , 𝐶 ⟩ } ‘ 𝑘 ) ) ) )
93 fnpr2o ( ( ( 𝐴 · 𝐵 ) ∈ 𝑋 ∧ ( 𝐴 × 𝐶 ) ∈ 𝑌 ) → { ⟨ ∅ , ( 𝐴 · 𝐵 ) ⟩ , ⟨ 1o , ( 𝐴 × 𝐶 ) ⟩ } Fn 2o )
94 14 15 93 syl2anc ( 𝜑 → { ⟨ ∅ , ( 𝐴 · 𝐵 ) ⟩ , ⟨ 1o , ( 𝐴 × 𝐶 ) ⟩ } Fn 2o )
95 dffn5 ( { ⟨ ∅ , ( 𝐴 · 𝐵 ) ⟩ , ⟨ 1o , ( 𝐴 × 𝐶 ) ⟩ } Fn 2o ↔ { ⟨ ∅ , ( 𝐴 · 𝐵 ) ⟩ , ⟨ 1o , ( 𝐴 × 𝐶 ) ⟩ } = ( 𝑘 ∈ 2o ↦ ( { ⟨ ∅ , ( 𝐴 · 𝐵 ) ⟩ , ⟨ 1o , ( 𝐴 × 𝐶 ) ⟩ } ‘ 𝑘 ) ) )
96 94 95 sylib ( 𝜑 → { ⟨ ∅ , ( 𝐴 · 𝐵 ) ⟩ , ⟨ 1o , ( 𝐴 × 𝐶 ) ⟩ } = ( 𝑘 ∈ 2o ↦ ( { ⟨ ∅ , ( 𝐴 · 𝐵 ) ⟩ , ⟨ 1o , ( 𝐴 × 𝐶 ) ⟩ } ‘ 𝑘 ) ) )
97 84 92 96 3eqtr4d ( 𝜑 → ( 𝐴 ( ·𝑠 ‘ ( 𝐺 Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ) { ⟨ ∅ , 𝐵 ⟩ , ⟨ 1o , 𝐶 ⟩ } ) = { ⟨ ∅ , ( 𝐴 · 𝐵 ) ⟩ , ⟨ 1o , ( 𝐴 × 𝐶 ) ⟩ } )
98 97 fveq2d ( 𝜑 → ( ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ‘ ( 𝐴 ( ·𝑠 ‘ ( 𝐺 Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ) { ⟨ ∅ , 𝐵 ⟩ , ⟨ 1o , 𝐶 ⟩ } ) ) = ( ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ‘ { ⟨ ∅ , ( 𝐴 · 𝐵 ) ⟩ , ⟨ 1o , ( 𝐴 × 𝐶 ) ⟩ } ) )
99 df-ov ( ( 𝐴 · 𝐵 ) ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ( 𝐴 × 𝐶 ) ) = ( ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ‘ ⟨ ( 𝐴 · 𝐵 ) , ( 𝐴 × 𝐶 ) ⟩ )
100 17 xpsfval ( ( ( 𝐴 · 𝐵 ) ∈ 𝑋 ∧ ( 𝐴 × 𝐶 ) ∈ 𝑌 ) → ( ( 𝐴 · 𝐵 ) ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ( 𝐴 × 𝐶 ) ) = { ⟨ ∅ , ( 𝐴 · 𝐵 ) ⟩ , ⟨ 1o , ( 𝐴 × 𝐶 ) ⟩ } )
101 14 15 100 syl2anc ( 𝜑 → ( ( 𝐴 · 𝐵 ) ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ( 𝐴 × 𝐶 ) ) = { ⟨ ∅ , ( 𝐴 · 𝐵 ) ⟩ , ⟨ 1o , ( 𝐴 × 𝐶 ) ⟩ } )
102 99 101 eqtr3id ( 𝜑 → ( ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ‘ ⟨ ( 𝐴 · 𝐵 ) , ( 𝐴 × 𝐶 ) ⟩ ) = { ⟨ ∅ , ( 𝐴 · 𝐵 ) ⟩ , ⟨ 1o , ( 𝐴 × 𝐶 ) ⟩ } )
103 14 15 opelxpd ( 𝜑 → ⟨ ( 𝐴 · 𝐵 ) , ( 𝐴 × 𝐶 ) ⟩ ∈ ( 𝑋 × 𝑌 ) )
104 f1ocnvfv ( ( ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) : ( 𝑋 × 𝑌 ) –1-1-onto→ ran ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ∧ ⟨ ( 𝐴 · 𝐵 ) , ( 𝐴 × 𝐶 ) ⟩ ∈ ( 𝑋 × 𝑌 ) ) → ( ( ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ‘ ⟨ ( 𝐴 · 𝐵 ) , ( 𝐴 × 𝐶 ) ⟩ ) = { ⟨ ∅ , ( 𝐴 · 𝐵 ) ⟩ , ⟨ 1o , ( 𝐴 × 𝐶 ) ⟩ } → ( ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ‘ { ⟨ ∅ , ( 𝐴 · 𝐵 ) ⟩ , ⟨ 1o , ( 𝐴 × 𝐶 ) ⟩ } ) = ⟨ ( 𝐴 · 𝐵 ) , ( 𝐴 × 𝐶 ) ⟩ ) )
105 22 103 104 sylancr ( 𝜑 → ( ( ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ‘ ⟨ ( 𝐴 · 𝐵 ) , ( 𝐴 × 𝐶 ) ⟩ ) = { ⟨ ∅ , ( 𝐴 · 𝐵 ) ⟩ , ⟨ 1o , ( 𝐴 × 𝐶 ) ⟩ } → ( ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ‘ { ⟨ ∅ , ( 𝐴 · 𝐵 ) ⟩ , ⟨ 1o , ( 𝐴 × 𝐶 ) ⟩ } ) = ⟨ ( 𝐴 · 𝐵 ) , ( 𝐴 × 𝐶 ) ⟩ ) )
106 102 105 mpd ( 𝜑 → ( ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ‘ { ⟨ ∅ , ( 𝐴 · 𝐵 ) ⟩ , ⟨ 1o , ( 𝐴 × 𝐶 ) ⟩ } ) = ⟨ ( 𝐴 · 𝐵 ) , ( 𝐴 × 𝐶 ) ⟩ )
107 98 106 eqtrd ( 𝜑 → ( ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ‘ ( 𝐴 ( ·𝑠 ‘ ( 𝐺 Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ) { ⟨ ∅ , 𝐵 ⟩ , ⟨ 1o , 𝐶 ⟩ } ) ) = ⟨ ( 𝐴 · 𝐵 ) , ( 𝐴 × 𝐶 ) ⟩ )
108 45 49 107 3eqtr3d ( 𝜑 → ( 𝐴 𝐵 , 𝐶 ⟩ ) = ⟨ ( 𝐴 · 𝐵 ) , ( 𝐴 × 𝐶 ) ⟩ )