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 ffvelcdmi ⊢ ( ⟨ 𝐵 , 𝐶 ⟩ ∈ ( 𝑋 × 𝑌 ) → ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 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 ⊢ ( 𝜑 → ( 𝐴 ∙ ⟨ 𝐵 , 𝐶 ⟩ ) = ⟨ ( 𝐴 · 𝐵 ) , ( 𝐴 × 𝐶 ) ⟩ )