Metamath Proof Explorer

Theorem xpsaddlem

Description: Lemma for xpsadd and xpsmul . (Contributed by Mario Carneiro, 15-Aug-2015)

Ref Expression
Hypotheses xpsval.t ⊢ 𝑇 = ( 𝑅 ×s 𝑆 )
xpsval.x ⊢ 𝑋 = ( Base ‘ 𝑅 )
xpsval.y ⊢ 𝑌 = ( Base ‘ 𝑆 )
xpsval.1 ⊢ ( 𝜑 → 𝑅 ∈ 𝑉 )
xpsval.2 ⊢ ( 𝜑 → 𝑆 ∈ 𝑊 )
xpsadd.3 ⊢ ( 𝜑 → 𝐴 ∈ 𝑋 )
xpsadd.4 ⊢ ( 𝜑 → 𝐵 ∈ 𝑌 )
xpsadd.5 ⊢ ( 𝜑 → 𝐶 ∈ 𝑋 )
xpsadd.6 ⊢ ( 𝜑 → 𝐷 ∈ 𝑌 )
xpsadd.7 ⊢ ( 𝜑 → ( 𝐴 · 𝐶 ) ∈ 𝑋 )
xpsadd.8 ⊢ ( 𝜑 → ( 𝐵 × 𝐷 ) ∈ 𝑌 )
xpsaddlem.m ⊢ · = ( 𝐸 ‘ 𝑅 )
xpsaddlem.n ⊢ × = ( 𝐸 ‘ 𝑆 )
xpsaddlem.p ⊢ ∙ = ( 𝐸 ‘ 𝑇 )
xpsaddlem.f ⊢ 𝐹 = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } )
xpsaddlem.u ⊢ 𝑈 = ( ( Scalar ‘ 𝑅 ) Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } )
xpsaddlem.1 ⊢ ( ( 𝜑 ∧ { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } ∈ ran 𝐹 ∧ { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } ∈ ran 𝐹 ) → ( ( ◡ 𝐹 ‘ { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } ) ∙ ( ◡ 𝐹 ‘ { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } ) ) = ( ◡ 𝐹 ‘ ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } ( 𝐸 ‘ 𝑈 ) { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } ) ) )
xpsaddlem.2 ⊢ ( ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } Fn 2o ∧ { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } ∈ ( Base ‘ 𝑈 ) ∧ { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } ∈ ( Base ‘ 𝑈 ) ) → ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } ( 𝐸 ‘ 𝑈 ) { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } ) = ( 𝑘 ∈ 2o ↦ ( ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } ‘ 𝑘 ) ( 𝐸 ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) ( { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } ‘ 𝑘 ) ) ) )
Assertion xpsaddlem ( 𝜑 → ( ⟨ 𝐴 , 𝐵 ⟩ ∙ ⟨ 𝐶 , 𝐷 ⟩ ) = ⟨ ( 𝐴 · 𝐶 ) , ( 𝐵 × 𝐷 ) ⟩ )

Proof

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