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 eqtr3id ( 𝜑 → ( 𝐹 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = { ⟨ ∅ , 𝐴 ⟩ , ⟨ 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 eqtr3id ( 𝜑 → ( 𝐹 ‘ ⟨ 𝐶 , 𝐷 ⟩ ) = { ⟨ ∅ , 𝐶 ⟩ , ⟨ 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 eqtr4di ( 𝑘 = ∅ → ( 𝐸 ‘ 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 eqtr4di ( ¬ 𝑘 = ∅ → ( 𝐸 ‘ 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 eqtr3id ( 𝜑 → ( 𝐹 ‘ ⟨ ( 𝐴 · 𝐶 ) , ( 𝐵 × 𝐷 ) ⟩ ) = { ⟨ ∅ , ( 𝐴 · 𝐶 ) ⟩ , ⟨ 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 ( 𝜑 → ( ⟨ 𝐴 , 𝐵𝐶 , 𝐷 ⟩ ) = ⟨ ( 𝐴 · 𝐶 ) , ( 𝐵 × 𝐷 ) ⟩ )