xpsmul

Description: Value of the multiplication 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	⊢ ( 𝜑 → ( 𝐵 × 𝐷 ) ∈ 𝑌 )
	xpsmul.m	⊢ · = ( ._r ‘ 𝑅 )
	xpsmul.n	⊢ × = ( ._r ‘ 𝑆 )
	xpsmul.p	⊢ ∙ = ( ._r ‘ 𝑇 )
Assertion	xpsmul	⊢ ( 𝜑 → ( ⟨ 𝐴 , 𝐵 ⟩ ∙ ⟨ 𝐶 , 𝐷 ⟩ ) = ⟨ ( 𝐴 · 𝐶 ) , ( 𝐵 × 𝐷 ) ⟩ )

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

Metamath Proof Explorer

Theorem xpsmul

Proof