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	⊢ ( 𝐵 ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) 𝐶 ) = ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) ‘ ⟨ 𝐵 , 𝐶 ⟩ )
17		eqid	⊢ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } )
18	17	xpsfval	⊢ ( ( 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑌 ) → ( 𝐵 ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) 𝐶 ) = { ⟨ ∅ , 𝐵 ⟩ , ⟨ 1_o , 𝐶 ⟩ } )
19	12 13 18	syl2anc	⊢ ( 𝜑 → ( 𝐵 ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) 𝐶 ) = { ⟨ ∅ , 𝐵 ⟩ , ⟨ 1_o , 𝐶 ⟩ } )
20	16 19	eqtr3id	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) ‘ ⟨ 𝐵 , 𝐶 ⟩ ) = { ⟨ ∅ , 𝐵 ⟩ , ⟨ 1_o , 𝐶 ⟩ } )
21	12 13	opelxpd	⊢ ( 𝜑 → ⟨ 𝐵 , 𝐶 ⟩ ∈ ( 𝑋 × 𝑌 ) )
22	17	xpsff1o2	⊢ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) : ( 𝑋 × 𝑌 ) –1-1-onto→ ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } )
23		f1of	⊢ ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) : ( 𝑋 × 𝑌 ) –1-1-onto→ ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) : ( 𝑋 × 𝑌 ) ⟶ ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) )
24	22 23	ax-mp	⊢ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) : ( 𝑋 × 𝑌 ) ⟶ ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } )
25	24	ffvelrni	⊢ ( ⟨ 𝐵 , 𝐶 ⟩ ∈ ( 𝑋 × 𝑌 ) → ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) ‘ ⟨ 𝐵 , 𝐶 ⟩ ) ∈ ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) )
26	21 25	syl	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) ‘ ⟨ 𝐵 , 𝐶 ⟩ ) ∈ ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) )
27	20 26	eqeltrrd	⊢ ( 𝜑 → { ⟨ ∅ , 𝐵 ⟩ , ⟨ 1_o , 𝐶 ⟩ } ∈ ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) )
28		eqid	⊢ ( 𝐺 X_s { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ) = ( 𝐺 X_s { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } )
29	1 5 6 3 4 17 2 28	xpsval	⊢ ( 𝜑 → 𝑇 = ( ^◡ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) “_s ( 𝐺 X_s { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ) ) )
30	1 5 6 3 4 17 2 28	xpsrnbas	⊢ ( 𝜑 → ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) = ( Base ‘ ( 𝐺 X_s { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ) ) )
31		f1ocnv	⊢ ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) : ( 𝑋 × 𝑌 ) –1-1-onto→ ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) → ^◡ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) : ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) –1-1-onto→ ( 𝑋 × 𝑌 ) )
32	22 31	mp1i	⊢ ( 𝜑 → ^◡ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) : ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) –1-1-onto→ ( 𝑋 × 𝑌 ) )
33		f1ofo	⊢ ( ^◡ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) : ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) –1-1-onto→ ( 𝑋 × 𝑌 ) → ^◡ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) : ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) –onto→ ( 𝑋 × 𝑌 ) )
34	32 33	syl	⊢ ( 𝜑 → ^◡ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) : ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) –onto→ ( 𝑋 × 𝑌 ) )
35		ovexd	⊢ ( 𝜑 → ( 𝐺 X_s { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ) ∈ V )
36	2	fvexi	⊢ 𝐺 ∈ V
37	36	a1i	⊢ ( ⊤ → 𝐺 ∈ V )
38		prex	⊢ { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ∈ V
39	38	a1i	⊢ ( ⊤ → { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ∈ V )
40	28 37 39	prdssca	⊢ ( ⊤ → 𝐺 = ( Scalar ‘ ( 𝐺 X_s { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ) ) )
41	40	mptru	⊢ 𝐺 = ( Scalar ‘ ( 𝐺 X_s { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ) )
42		eqid	⊢ ( ·_𝑠 ‘ ( 𝐺 X_s { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ) ) = ( ·_𝑠 ‘ ( 𝐺 X_s { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ) )
43	32	f1ovscpbl	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) ∧ 𝑐 ∈ ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) ) ) → ( ( ^◡ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) ‘ 𝑏 ) = ( ^◡ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) ‘ 𝑐 ) → ( ^◡ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) ‘ ( 𝑎 ( ·_𝑠 ‘ ( 𝐺 X_s { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ) ) 𝑏 ) ) = ( ^◡ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) ‘ ( 𝑎 ( ·_𝑠 ‘ ( 𝐺 X_s { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ) ) 𝑐 ) ) ) )
44	29 30 34 35 41 7 42 10 43	imasvscaval	⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝐾 ∧ { ⟨ ∅ , 𝐵 ⟩ , ⟨ 1_o , 𝐶 ⟩ } ∈ ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) ) → ( 𝐴 ∙ ( ^◡ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) ‘ { ⟨ ∅ , 𝐵 ⟩ , ⟨ 1_o , 𝐶 ⟩ } ) ) = ( ^◡ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) ‘ ( 𝐴 ( ·_𝑠 ‘ ( 𝐺 X_s { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ) ) { ⟨ ∅ , 𝐵 ⟩ , ⟨ 1_o , 𝐶 ⟩ } ) ) )
45	11 27 44	mpd3an23	⊢ ( 𝜑 → ( 𝐴 ∙ ( ^◡ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) ‘ { ⟨ ∅ , 𝐵 ⟩ , ⟨ 1_o , 𝐶 ⟩ } ) ) = ( ^◡ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) ‘ ( 𝐴 ( ·_𝑠 ‘ ( 𝐺 X_s { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ) ) { ⟨ ∅ , 𝐵 ⟩ , ⟨ 1_o , 𝐶 ⟩ } ) ) )
46		f1ocnvfv	⊢ ( ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) : ( 𝑋 × 𝑌 ) –1-1-onto→ ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) ∧ ⟨ 𝐵 , 𝐶 ⟩ ∈ ( 𝑋 × 𝑌 ) ) → ( ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) ‘ ⟨ 𝐵 , 𝐶 ⟩ ) = { ⟨ ∅ , 𝐵 ⟩ , ⟨ 1_o , 𝐶 ⟩ } → ( ^◡ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) ‘ { ⟨ ∅ , 𝐵 ⟩ , ⟨ 1_o , 𝐶 ⟩ } ) = ⟨ 𝐵 , 𝐶 ⟩ ) )
47	22 21 46	sylancr	⊢ ( 𝜑 → ( ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) ‘ ⟨ 𝐵 , 𝐶 ⟩ ) = { ⟨ ∅ , 𝐵 ⟩ , ⟨ 1_o , 𝐶 ⟩ } → ( ^◡ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) ‘ { ⟨ ∅ , 𝐵 ⟩ , ⟨ 1_o , 𝐶 ⟩ } ) = ⟨ 𝐵 , 𝐶 ⟩ ) )
48	20 47	mpd	⊢ ( 𝜑 → ( ^◡ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) ‘ { ⟨ ∅ , 𝐵 ⟩ , ⟨ 1_o , 𝐶 ⟩ } ) = ⟨ 𝐵 , 𝐶 ⟩ )
49	48	oveq2d	⊢ ( 𝜑 → ( 𝐴 ∙ ( ^◡ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) ‘ { ⟨ ∅ , 𝐵 ⟩ , ⟨ 1_o , 𝐶 ⟩ } ) ) = ( 𝐴 ∙ ⟨ 𝐵 , 𝐶 ⟩ ) )
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	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 2_o ) → 𝑅 ∈ 𝑉 )
68	4	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 2_o ) → 𝑆 ∈ 𝑊 )
69		simpr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 2_o ) → 𝑘 ∈ 2_o )
70		fvprif	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝑘 ∈ 2_o ) → ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) = if ( 𝑘 = ∅ , 𝑅 , 𝑆 ) )
71	67 68 69 70	syl3anc	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 2_o ) → ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) = if ( 𝑘 = ∅ , 𝑅 , 𝑆 ) )
72	71	fveq2d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 2_o ) → ( ·_𝑠 ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) = ( ·_𝑠 ‘ if ( 𝑘 = ∅ , 𝑅 , 𝑆 ) ) )
73		eqidd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 2_o ) → 𝐴 = 𝐴 )
74	12	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 2_o ) → 𝐵 ∈ 𝑋 )
75	13	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 2_o ) → 𝐶 ∈ 𝑌 )
76		fvprif	⊢ ( ( 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑌 ∧ 𝑘 ∈ 2_o ) → ( { ⟨ ∅ , 𝐵 ⟩ , ⟨ 1_o , 𝐶 ⟩ } ‘ 𝑘 ) = if ( 𝑘 = ∅ , 𝐵 , 𝐶 ) )
77	74 75 69 76	syl3anc	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 2_o ) → ( { ⟨ ∅ , 𝐵 ⟩ , ⟨ 1_o , 𝐶 ⟩ } ‘ 𝑘 ) = if ( 𝑘 = ∅ , 𝐵 , 𝐶 ) )
78	72 73 77	oveq123d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 2_o ) → ( 𝐴 ( ·_𝑠 ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) ( { ⟨ ∅ , 𝐵 ⟩ , ⟨ 1_o , 𝐶 ⟩ } ‘ 𝑘 ) ) = ( 𝐴 ( ·_𝑠 ‘ if ( 𝑘 = ∅ , 𝑅 , 𝑆 ) ) if ( 𝑘 = ∅ , 𝐵 , 𝐶 ) ) )
79	14	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 2_o ) → ( 𝐴 · 𝐵 ) ∈ 𝑋 )
80	15	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 2_o ) → ( 𝐴 × 𝐶 ) ∈ 𝑌 )
81		fvprif	⊢ ( ( ( 𝐴 · 𝐵 ) ∈ 𝑋 ∧ ( 𝐴 × 𝐶 ) ∈ 𝑌 ∧ 𝑘 ∈ 2_o ) → ( { ⟨ ∅ , ( 𝐴 · 𝐵 ) ⟩ , ⟨ 1_o , ( 𝐴 × 𝐶 ) ⟩ } ‘ 𝑘 ) = if ( 𝑘 = ∅ , ( 𝐴 · 𝐵 ) , ( 𝐴 × 𝐶 ) ) )
82	79 80 69 81	syl3anc	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 2_o ) → ( { ⟨ ∅ , ( 𝐴 · 𝐵 ) ⟩ , ⟨ 1_o , ( 𝐴 × 𝐶 ) ⟩ } ‘ 𝑘 ) = if ( 𝑘 = ∅ , ( 𝐴 · 𝐵 ) , ( 𝐴 × 𝐶 ) ) )
83	66 78 82	3eqtr4a	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 2_o ) → ( 𝐴 ( ·_𝑠 ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) ( { ⟨ ∅ , 𝐵 ⟩ , ⟨ 1_o , 𝐶 ⟩ } ‘ 𝑘 ) ) = ( { ⟨ ∅ , ( 𝐴 · 𝐵 ) ⟩ , ⟨ 1_o , ( 𝐴 × 𝐶 ) ⟩ } ‘ 𝑘 ) )
84	83	mpteq2dva	⊢ ( 𝜑 → ( 𝑘 ∈ 2_o ↦ ( 𝐴 ( ·_𝑠 ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) ( { ⟨ ∅ , 𝐵 ⟩ , ⟨ 1_o , 𝐶 ⟩ } ‘ 𝑘 ) ) ) = ( 𝑘 ∈ 2_o ↦ ( { ⟨ ∅ , ( 𝐴 · 𝐵 ) ⟩ , ⟨ 1_o , ( 𝐴 × 𝐶 ) ⟩ } ‘ 𝑘 ) ) )
85		eqid	⊢ ( Base ‘ ( 𝐺 X_s { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ) ) = ( Base ‘ ( 𝐺 X_s { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ) )
86	36	a1i	⊢ ( 𝜑 → 𝐺 ∈ V )
87		2on	⊢ 2_o ∈ On
88	87	a1i	⊢ ( 𝜑 → 2_o ∈ On )
89		fnpr2o	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ) → { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } Fn 2_o )
90	3 4 89	syl2anc	⊢ ( 𝜑 → { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } Fn 2_o )
91	27 30	eleqtrd	⊢ ( 𝜑 → { ⟨ ∅ , 𝐵 ⟩ , ⟨ 1_o , 𝐶 ⟩ } ∈ ( Base ‘ ( 𝐺 X_s { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ) ) )
92	28 85 42 7 86 88 90 11 91	prdsvscaval	⊢ ( 𝜑 → ( 𝐴 ( ·_𝑠 ‘ ( 𝐺 X_s { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ) ) { ⟨ ∅ , 𝐵 ⟩ , ⟨ 1_o , 𝐶 ⟩ } ) = ( 𝑘 ∈ 2_o ↦ ( 𝐴 ( ·_𝑠 ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) ( { ⟨ ∅ , 𝐵 ⟩ , ⟨ 1_o , 𝐶 ⟩ } ‘ 𝑘 ) ) ) )
93		fnpr2o	⊢ ( ( ( 𝐴 · 𝐵 ) ∈ 𝑋 ∧ ( 𝐴 × 𝐶 ) ∈ 𝑌 ) → { ⟨ ∅ , ( 𝐴 · 𝐵 ) ⟩ , ⟨ 1_o , ( 𝐴 × 𝐶 ) ⟩ } Fn 2_o )
94	14 15 93	syl2anc	⊢ ( 𝜑 → { ⟨ ∅ , ( 𝐴 · 𝐵 ) ⟩ , ⟨ 1_o , ( 𝐴 × 𝐶 ) ⟩ } Fn 2_o )
95		dffn5	⊢ ( { ⟨ ∅ , ( 𝐴 · 𝐵 ) ⟩ , ⟨ 1_o , ( 𝐴 × 𝐶 ) ⟩ } Fn 2_o ↔ { ⟨ ∅ , ( 𝐴 · 𝐵 ) ⟩ , ⟨ 1_o , ( 𝐴 × 𝐶 ) ⟩ } = ( 𝑘 ∈ 2_o ↦ ( { ⟨ ∅ , ( 𝐴 · 𝐵 ) ⟩ , ⟨ 1_o , ( 𝐴 × 𝐶 ) ⟩ } ‘ 𝑘 ) ) )
96	94 95	sylib	⊢ ( 𝜑 → { ⟨ ∅ , ( 𝐴 · 𝐵 ) ⟩ , ⟨ 1_o , ( 𝐴 × 𝐶 ) ⟩ } = ( 𝑘 ∈ 2_o ↦ ( { ⟨ ∅ , ( 𝐴 · 𝐵 ) ⟩ , ⟨ 1_o , ( 𝐴 × 𝐶 ) ⟩ } ‘ 𝑘 ) ) )
97	84 92 96	3eqtr4d	⊢ ( 𝜑 → ( 𝐴 ( ·_𝑠 ‘ ( 𝐺 X_s { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ) ) { ⟨ ∅ , 𝐵 ⟩ , ⟨ 1_o , 𝐶 ⟩ } ) = { ⟨ ∅ , ( 𝐴 · 𝐵 ) ⟩ , ⟨ 1_o , ( 𝐴 × 𝐶 ) ⟩ } )
98	97	fveq2d	⊢ ( 𝜑 → ( ^◡ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) ‘ ( 𝐴 ( ·_𝑠 ‘ ( 𝐺 X_s { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ) ) { ⟨ ∅ , 𝐵 ⟩ , ⟨ 1_o , 𝐶 ⟩ } ) ) = ( ^◡ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) ‘ { ⟨ ∅ , ( 𝐴 · 𝐵 ) ⟩ , ⟨ 1_o , ( 𝐴 × 𝐶 ) ⟩ } ) )
99		df-ov	⊢ ( ( 𝐴 · 𝐵 ) ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) ( 𝐴 × 𝐶 ) ) = ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) ‘ ⟨ ( 𝐴 · 𝐵 ) , ( 𝐴 × 𝐶 ) ⟩ )
100	17	xpsfval	⊢ ( ( ( 𝐴 · 𝐵 ) ∈ 𝑋 ∧ ( 𝐴 × 𝐶 ) ∈ 𝑌 ) → ( ( 𝐴 · 𝐵 ) ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) ( 𝐴 × 𝐶 ) ) = { ⟨ ∅ , ( 𝐴 · 𝐵 ) ⟩ , ⟨ 1_o , ( 𝐴 × 𝐶 ) ⟩ } )
101	14 15 100	syl2anc	⊢ ( 𝜑 → ( ( 𝐴 · 𝐵 ) ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) ( 𝐴 × 𝐶 ) ) = { ⟨ ∅ , ( 𝐴 · 𝐵 ) ⟩ , ⟨ 1_o , ( 𝐴 × 𝐶 ) ⟩ } )
102	99 101	eqtr3id	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) ‘ ⟨ ( 𝐴 · 𝐵 ) , ( 𝐴 × 𝐶 ) ⟩ ) = { ⟨ ∅ , ( 𝐴 · 𝐵 ) ⟩ , ⟨ 1_o , ( 𝐴 × 𝐶 ) ⟩ } )
103	14 15	opelxpd	⊢ ( 𝜑 → ⟨ ( 𝐴 · 𝐵 ) , ( 𝐴 × 𝐶 ) ⟩ ∈ ( 𝑋 × 𝑌 ) )
104		f1ocnvfv	⊢ ( ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) : ( 𝑋 × 𝑌 ) –1-1-onto→ ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) ∧ ⟨ ( 𝐴 · 𝐵 ) , ( 𝐴 × 𝐶 ) ⟩ ∈ ( 𝑋 × 𝑌 ) ) → ( ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) ‘ ⟨ ( 𝐴 · 𝐵 ) , ( 𝐴 × 𝐶 ) ⟩ ) = { ⟨ ∅ , ( 𝐴 · 𝐵 ) ⟩ , ⟨ 1_o , ( 𝐴 × 𝐶 ) ⟩ } → ( ^◡ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) ‘ { ⟨ ∅ , ( 𝐴 · 𝐵 ) ⟩ , ⟨ 1_o , ( 𝐴 × 𝐶 ) ⟩ } ) = ⟨ ( 𝐴 · 𝐵 ) , ( 𝐴 × 𝐶 ) ⟩ ) )
105	22 103 104	sylancr	⊢ ( 𝜑 → ( ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) ‘ ⟨ ( 𝐴 · 𝐵 ) , ( 𝐴 × 𝐶 ) ⟩ ) = { ⟨ ∅ , ( 𝐴 · 𝐵 ) ⟩ , ⟨ 1_o , ( 𝐴 × 𝐶 ) ⟩ } → ( ^◡ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) ‘ { ⟨ ∅ , ( 𝐴 · 𝐵 ) ⟩ , ⟨ 1_o , ( 𝐴 × 𝐶 ) ⟩ } ) = ⟨ ( 𝐴 · 𝐵 ) , ( 𝐴 × 𝐶 ) ⟩ ) )
106	102 105	mpd	⊢ ( 𝜑 → ( ^◡ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) ‘ { ⟨ ∅ , ( 𝐴 · 𝐵 ) ⟩ , ⟨ 1_o , ( 𝐴 × 𝐶 ) ⟩ } ) = ⟨ ( 𝐴 · 𝐵 ) , ( 𝐴 × 𝐶 ) ⟩ )
107	98 106	eqtrd	⊢ ( 𝜑 → ( ^◡ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) ‘ ( 𝐴 ( ·_𝑠 ‘ ( 𝐺 X_s { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ) ) { ⟨ ∅ , 𝐵 ⟩ , ⟨ 1_o , 𝐶 ⟩ } ) ) = ⟨ ( 𝐴 · 𝐵 ) , ( 𝐴 × 𝐶 ) ⟩ )
108	45 49 107	3eqtr3d	⊢ ( 𝜑 → ( 𝐴 ∙ ⟨ 𝐵 , 𝐶 ⟩ ) = ⟨ ( 𝐴 · 𝐵 ) , ( 𝐴 × 𝐶 ) ⟩ )

Metamath Proof Explorer

Theorem xpsvsca

Proof