Metamath Proof Explorer


Theorem xpsadd

Description: Value of the addition operation in a binary structure product. (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 ( 𝜑 → ( 𝐵 × 𝐷 ) ∈ 𝑌 )
xpsadd.m · = ( +g𝑅 )
xpsadd.n × = ( +g𝑆 )
xpsadd.p = ( +g𝑇 )
Assertion xpsadd ( 𝜑 → ( ⟨ 𝐴 , 𝐵𝐶 , 𝐷 ⟩ ) = ⟨ ( 𝐴 · 𝐶 ) , ( 𝐵 × 𝐷 ) ⟩ )

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 xpsadd.m · = ( +g𝑅 )
13 xpsadd.n × = ( +g𝑆 )
14 xpsadd.p = ( +g𝑇 )
15 eqid ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) = ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } )
16 eqid ( ( Scalar ‘ 𝑅 ) Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) = ( ( Scalar ‘ 𝑅 ) Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } )
17 15 xpsff1o2 ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) : ( 𝑋 × 𝑌 ) –1-1-onto→ ran ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } )
18 f1ocnv ( ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) : ( 𝑋 × 𝑌 ) –1-1-onto→ ran ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) → ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) : ran ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) –1-1-onto→ ( 𝑋 × 𝑌 ) )
19 17 18 mp1i ( 𝜑 ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) : ran ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) –1-1-onto→ ( 𝑋 × 𝑌 ) )
20 f1ofo ( ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) : ran ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) –1-1-onto→ ( 𝑋 × 𝑌 ) → ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) : ran ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) –onto→ ( 𝑋 × 𝑌 ) )
21 19 20 syl ( 𝜑 ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) : ran ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) –onto→ ( 𝑋 × 𝑌 ) )
22 19 f1ocpbl ( ( 𝜑 ∧ ( 𝑎 ∈ ran ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ∧ 𝑏 ∈ ran ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ) ∧ ( 𝑐 ∈ ran ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ∧ 𝑑 ∈ ran ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ) ) → ( ( ( ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ‘ 𝑎 ) = ( ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ‘ 𝑐 ) ∧ ( ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ‘ 𝑏 ) = ( ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ‘ 𝑑 ) ) → ( ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ‘ ( 𝑎 ( +g ‘ ( ( Scalar ‘ 𝑅 ) Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ) 𝑏 ) ) = ( ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ‘ ( 𝑐 ( +g ‘ ( ( Scalar ‘ 𝑅 ) Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ) 𝑑 ) ) ) )
23 eqid ( Scalar ‘ 𝑅 ) = ( Scalar ‘ 𝑅 )
24 1 2 3 4 5 15 23 16 xpsval ( 𝜑𝑇 = ( ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) “s ( ( Scalar ‘ 𝑅 ) Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ) )
25 1 2 3 4 5 15 23 16 xpsrnbas ( 𝜑 → ran ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) = ( Base ‘ ( ( Scalar ‘ 𝑅 ) Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ) )
26 ovexd ( 𝜑 → ( ( Scalar ‘ 𝑅 ) Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ∈ V )
27 eqid ( +g ‘ ( ( Scalar ‘ 𝑅 ) Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ) = ( +g ‘ ( ( Scalar ‘ 𝑅 ) Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) )
28 21 22 24 25 26 27 14 imasaddval ( ( 𝜑 ∧ { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } ∈ ran ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ∧ { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } ∈ ran ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ) → ( ( ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ‘ { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } ) ( ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ‘ { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } ) ) = ( ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ‘ ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } ( +g ‘ ( ( Scalar ‘ 𝑅 ) Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ) { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } ) ) )
29 eqid ( Base ‘ ( ( Scalar ‘ 𝑅 ) Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ) = ( Base ‘ ( ( Scalar ‘ 𝑅 ) Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) )
30 fvexd ( ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } Fn 2o ∧ { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } ∈ ( Base ‘ ( ( Scalar ‘ 𝑅 ) Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ) ∧ { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } ∈ ( Base ‘ ( ( Scalar ‘ 𝑅 ) Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ) ) → ( Scalar ‘ 𝑅 ) ∈ V )
31 2on 2o ∈ On
32 31 a1i ( ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } Fn 2o ∧ { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } ∈ ( Base ‘ ( ( Scalar ‘ 𝑅 ) Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ) ∧ { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } ∈ ( Base ‘ ( ( Scalar ‘ 𝑅 ) Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ) ) → 2o ∈ On )
33 simp1 ( ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } Fn 2o ∧ { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } ∈ ( Base ‘ ( ( Scalar ‘ 𝑅 ) Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ) ∧ { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } ∈ ( Base ‘ ( ( Scalar ‘ 𝑅 ) Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ) ) → { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } Fn 2o )
34 simp2 ( ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } Fn 2o ∧ { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } ∈ ( Base ‘ ( ( Scalar ‘ 𝑅 ) Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ) ∧ { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } ∈ ( Base ‘ ( ( Scalar ‘ 𝑅 ) Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ) ) → { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } ∈ ( Base ‘ ( ( Scalar ‘ 𝑅 ) Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ) )
35 simp3 ( ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } Fn 2o ∧ { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } ∈ ( Base ‘ ( ( Scalar ‘ 𝑅 ) Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ) ∧ { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } ∈ ( Base ‘ ( ( Scalar ‘ 𝑅 ) Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ) ) → { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } ∈ ( Base ‘ ( ( Scalar ‘ 𝑅 ) Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ) )
36 16 29 30 32 33 34 35 27 prdsplusgval ( ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } Fn 2o ∧ { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } ∈ ( Base ‘ ( ( Scalar ‘ 𝑅 ) Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ) ∧ { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } ∈ ( Base ‘ ( ( Scalar ‘ 𝑅 ) Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ) ) → ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } ( +g ‘ ( ( Scalar ‘ 𝑅 ) Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ) { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } ) = ( 𝑘 ∈ 2o ↦ ( ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } ‘ 𝑘 ) ( +g ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) ( { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } ‘ 𝑘 ) ) ) )
37 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 28 36 xpsaddlem ( 𝜑 → ( ⟨ 𝐴 , 𝐵𝐶 , 𝐷 ⟩ ) = ⟨ ( 𝐴 · 𝐶 ) , ( 𝐵 × 𝐷 ) ⟩ )