Theorem xpsvsca 16062

Description: Value of the scalar multiplication function in a binary structure product. (Contributed by Mario Carneiro, 15-Aug-2015.)

Hypotheses

Ref	Expression
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

Ref	Expression
xpsvsca	⊢ (𝜑 → (𝐴 ∙ ⟨𝐵, 𝐶⟩) = ⟨(𝐴 · 𝐵), (𝐴 × 𝐶)⟩)

Proof of Theorem xpsvsca

Dummy variables 𝑘 𝑎 𝑥 𝑦 𝑐 𝑏 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		xpsvsca.3	. . 3 ⊢ (𝜑 → 𝐴 ∈ 𝐾)
2		df-ov 6552	. . . . 5 ⊢ (𝐵(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))𝐶) = ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘⟨𝐵, 𝐶⟩)
3		xpsvsca.4	. . . . . 6 ⊢ (𝜑 → 𝐵 ∈ 𝑋)
4		xpsvsca.5	. . . . . 6 ⊢ (𝜑 → 𝐶 ∈ 𝑌)
5		eqid 2610	. . . . . . 7 ⊢ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))
6	5	xpsfval 16050	. . . . . 6 ⊢ ((𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑌) → (𝐵(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))𝐶) = ◡({𝐵} +𝑐 {𝐶}))
7	3, 4, 6	syl2anc 691	. . . . 5 ⊢ (𝜑 → (𝐵(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))𝐶) = ◡({𝐵} +𝑐 {𝐶}))
8	2, 7	syl5eqr 2658	. . . 4 ⊢ (𝜑 → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘⟨𝐵, 𝐶⟩) = ◡({𝐵} +𝑐 {𝐶}))
9		opelxpi 5072	. . . . . 6 ⊢ ((𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑌) → ⟨𝐵, 𝐶⟩ ∈ (𝑋 × 𝑌))
10	3, 4, 9	syl2anc 691	. . . . 5 ⊢ (𝜑 → ⟨𝐵, 𝐶⟩ ∈ (𝑋 × 𝑌))
11	5	xpsff1o2 16054	. . . . . . 7 ⊢ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})):(𝑋 × 𝑌)–1-1-onto→ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))
12		f1of 6050	. . . . . . 7 ⊢ ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})):(𝑋 × 𝑌)–1-1-onto→ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})):(𝑋 × 𝑌)⟶ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})))
13	11, 12	ax-mp 5	. . . . . 6 ⊢ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})):(𝑋 × 𝑌)⟶ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))
14	13	ffvelrni 6266	. . . . 5 ⊢ (⟨𝐵, 𝐶⟩ ∈ (𝑋 × 𝑌) → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘⟨𝐵, 𝐶⟩) ∈ ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})))
15	10, 14	syl 17	. . . 4 ⊢ (𝜑 → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘⟨𝐵, 𝐶⟩) ∈ ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})))
16	8, 15	eqeltrrd 2689	. . 3 ⊢ (𝜑 → ◡({𝐵} +𝑐 {𝐶}) ∈ ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})))
17		xpssca.t	. . . . 5 ⊢ 𝑇 = (𝑅 ×s 𝑆)
18		xpsvsca.x	. . . . 5 ⊢ 𝑋 = (Base‘𝑅)
19		xpsvsca.y	. . . . 5 ⊢ 𝑌 = (Base‘𝑆)
20		xpssca.1	. . . . 5 ⊢ (𝜑 → 𝑅 ∈ 𝑉)
21		xpssca.2	. . . . 5 ⊢ (𝜑 → 𝑆 ∈ 𝑊)
22		xpssca.g	. . . . 5 ⊢ 𝐺 = (Scalar‘𝑅)
23		eqid 2610	. . . . 5 ⊢ (𝐺Xs◡({𝑅} +𝑐 {𝑆})) = (𝐺Xs◡({𝑅} +𝑐 {𝑆}))
24	17, 18, 19, 20, 21, 5, 22, 23	xpsval 16055	. . . 4 ⊢ (𝜑 → 𝑇 = (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) “s (𝐺Xs◡({𝑅} +𝑐 {𝑆}))))
25	17, 18, 19, 20, 21, 5, 22, 23	xpslem 16056	. . . 4 ⊢ (𝜑 → ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) = (Base‘(𝐺Xs◡({𝑅} +𝑐 {𝑆}))))
26		f1ocnv 6062	. . . . . 6 ⊢ ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})):(𝑋 × 𝑌)–1-1-onto→ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) → ◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})):ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))–1-1-onto→(𝑋 × 𝑌))
27	11, 26	mp1i 13	. . . . 5 ⊢ (𝜑 → ◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})):ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))–1-1-onto→(𝑋 × 𝑌))
28		f1ofo 6057	. . . . 5 ⊢ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})):ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))–1-1-onto→(𝑋 × 𝑌) → ◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})):ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))–onto→(𝑋 × 𝑌))
29	27, 28	syl 17	. . . 4 ⊢ (𝜑 → ◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})):ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))–onto→(𝑋 × 𝑌))
30		ovex 6577	. . . . 5 ⊢ (𝐺Xs◡({𝑅} +𝑐 {𝑆})) ∈ V
31	30	a1i 11	. . . 4 ⊢ (𝜑 → (𝐺Xs◡({𝑅} +𝑐 {𝑆})) ∈ V)
32		fvex 6113	. . . . . . . 8 ⊢ (Scalar‘𝑅) ∈ V
33	22, 32	eqeltri 2684	. . . . . . 7 ⊢ 𝐺 ∈ V
34	33	a1i 11	. . . . . 6 ⊢ (⊤ → 𝐺 ∈ V)
35		ovex 6577	. . . . . . . 8 ⊢ ({𝑅} +𝑐 {𝑆}) ∈ V
36	35	cnvex 7006	. . . . . . 7 ⊢ ◡({𝑅} +𝑐 {𝑆}) ∈ V
37	36	a1i 11	. . . . . 6 ⊢ (⊤ → ◡({𝑅} +𝑐 {𝑆}) ∈ V)
38	23, 34, 37	prdssca 15939	. . . . 5 ⊢ (⊤ → 𝐺 = (Scalar‘(𝐺Xs◡({𝑅} +𝑐 {𝑆}))))
39	38	trud 1484	. . . 4 ⊢ 𝐺 = (Scalar‘(𝐺Xs◡({𝑅} +𝑐 {𝑆})))
40		xpsvsca.k	. . . 4 ⊢ 𝐾 = (Base‘𝐺)
41		eqid 2610	. . . 4 ⊢ ( ·𝑠 ‘(𝐺Xs◡({𝑅} +𝑐 {𝑆}))) = ( ·𝑠 ‘(𝐺Xs◡({𝑅} +𝑐 {𝑆})))
42		xpsvsca.p	. . . 4 ⊢ ∙ = ( ·𝑠 ‘𝑇)
43	27	f1ovscpbl 16009	. . . 4 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐾 ∧ 𝑏 ∈ ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) ∧ 𝑐 ∈ ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})))) → ((◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘𝑏) = (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘𝑐) → (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘(𝑎( ·𝑠 ‘(𝐺Xs◡({𝑅} +𝑐 {𝑆})))𝑏)) = (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘(𝑎( ·𝑠 ‘(𝐺Xs◡({𝑅} +𝑐 {𝑆})))𝑐))))
44	24, 25, 29, 31, 39, 40, 41, 42, 43	imasvscaval 16021	. . 3 ⊢ ((𝜑 ∧ 𝐴 ∈ 𝐾 ∧ ◡({𝐵} +𝑐 {𝐶}) ∈ ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))) → (𝐴 ∙ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘◡({𝐵} +𝑐 {𝐶}))) = (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘(𝐴( ·𝑠 ‘(𝐺Xs◡({𝑅} +𝑐 {𝑆})))◡({𝐵} +𝑐 {𝐶}))))
45	1, 16, 44	mpd3an23 1418	. 2 ⊢ (𝜑 → (𝐴 ∙ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘◡({𝐵} +𝑐 {𝐶}))) = (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘(𝐴( ·𝑠 ‘(𝐺Xs◡({𝑅} +𝑐 {𝑆})))◡({𝐵} +𝑐 {𝐶}))))
46		f1ocnvfv 6434	. . . . 5 ⊢ (((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})):(𝑋 × 𝑌)–1-1-onto→ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) ∧ ⟨𝐵, 𝐶⟩ ∈ (𝑋 × 𝑌)) → (((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘⟨𝐵, 𝐶⟩) = ◡({𝐵} +𝑐 {𝐶}) → (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘◡({𝐵} +𝑐 {𝐶})) = ⟨𝐵, 𝐶⟩))
47	11, 10, 46	sylancr 694	. . . 4 ⊢ (𝜑 → (((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘⟨𝐵, 𝐶⟩) = ◡({𝐵} +𝑐 {𝐶}) → (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘◡({𝐵} +𝑐 {𝐶})) = ⟨𝐵, 𝐶⟩))
48	8, 47	mpd 15	. . 3 ⊢ (𝜑 → (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘◡({𝐵} +𝑐 {𝐶})) = ⟨𝐵, 𝐶⟩)
49	48	oveq2d 6565	. 2 ⊢ (𝜑 → (𝐴 ∙ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘◡({𝐵} +𝑐 {𝐶}))) = (𝐴 ∙ ⟨𝐵, 𝐶⟩))
50		iftrue 4042	. . . . . . . . . . . 12 ⊢ (𝑘 = ∅ → if(𝑘 = ∅, 𝑅, 𝑆) = 𝑅)
51	50	fveq2d 6107	. . . . . . . . . . 11 ⊢ (𝑘 = ∅ → ( ·𝑠 ‘if(𝑘 = ∅, 𝑅, 𝑆)) = ( ·𝑠 ‘𝑅))
52		xpsvsca.m	. . . . . . . . . . 11 ⊢ · = ( ·𝑠 ‘𝑅)
53	51, 52	syl6eqr 2662	. . . . . . . . . 10 ⊢ (𝑘 = ∅ → ( ·𝑠 ‘if(𝑘 = ∅, 𝑅, 𝑆)) = · )
54		eqidd 2611	. . . . . . . . . 10 ⊢ (𝑘 = ∅ → 𝐴 = 𝐴)
55		iftrue 4042	. . . . . . . . . 10 ⊢ (𝑘 = ∅ → if(𝑘 = ∅, 𝐵, 𝐶) = 𝐵)
56	53, 54, 55	oveq123d 6570	. . . . . . . . 9 ⊢ (𝑘 = ∅ → (𝐴( ·𝑠 ‘if(𝑘 = ∅, 𝑅, 𝑆))if(𝑘 = ∅, 𝐵, 𝐶)) = (𝐴 · 𝐵))
57		iftrue 4042	. . . . . . . . 9 ⊢ (𝑘 = ∅ → if(𝑘 = ∅, (𝐴 · 𝐵), (𝐴 × 𝐶)) = (𝐴 · 𝐵))
58	56, 57	eqtr4d 2647	. . . . . . . 8 ⊢ (𝑘 = ∅ → (𝐴( ·𝑠 ‘if(𝑘 = ∅, 𝑅, 𝑆))if(𝑘 = ∅, 𝐵, 𝐶)) = if(𝑘 = ∅, (𝐴 · 𝐵), (𝐴 × 𝐶)))
59		iffalse 4045	. . . . . . . . . . . 12 ⊢ (¬ 𝑘 = ∅ → if(𝑘 = ∅, 𝑅, 𝑆) = 𝑆)
60	59	fveq2d 6107	. . . . . . . . . . 11 ⊢ (¬ 𝑘 = ∅ → ( ·𝑠 ‘if(𝑘 = ∅, 𝑅, 𝑆)) = ( ·𝑠 ‘𝑆))
61		xpsvsca.n	. . . . . . . . . . 11 ⊢ × = ( ·𝑠 ‘𝑆)
62	60, 61	syl6eqr 2662	. . . . . . . . . 10 ⊢ (¬ 𝑘 = ∅ → ( ·𝑠 ‘if(𝑘 = ∅, 𝑅, 𝑆)) = × )
63		eqidd 2611	. . . . . . . . . 10 ⊢ (¬ 𝑘 = ∅ → 𝐴 = 𝐴)
64		iffalse 4045	. . . . . . . . . 10 ⊢ (¬ 𝑘 = ∅ → if(𝑘 = ∅, 𝐵, 𝐶) = 𝐶)
65	62, 63, 64	oveq123d 6570	. . . . . . . . 9 ⊢ (¬ 𝑘 = ∅ → (𝐴( ·𝑠 ‘if(𝑘 = ∅, 𝑅, 𝑆))if(𝑘 = ∅, 𝐵, 𝐶)) = (𝐴 × 𝐶))
66		iffalse 4045	. . . . . . . . 9 ⊢ (¬ 𝑘 = ∅ → if(𝑘 = ∅, (𝐴 · 𝐵), (𝐴 × 𝐶)) = (𝐴 × 𝐶))
67	65, 66	eqtr4d 2647	. . . . . . . 8 ⊢ (¬ 𝑘 = ∅ → (𝐴( ·𝑠 ‘if(𝑘 = ∅, 𝑅, 𝑆))if(𝑘 = ∅, 𝐵, 𝐶)) = if(𝑘 = ∅, (𝐴 · 𝐵), (𝐴 × 𝐶)))
68	58, 67	pm2.61i 175	. . . . . . 7 ⊢ (𝐴( ·𝑠 ‘if(𝑘 = ∅, 𝑅, 𝑆))if(𝑘 = ∅, 𝐵, 𝐶)) = if(𝑘 = ∅, (𝐴 · 𝐵), (𝐴 × 𝐶))
69	20	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ 2𝑜) → 𝑅 ∈ 𝑉)
70	21	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ 2𝑜) → 𝑆 ∈ 𝑊)
71		simpr 476	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ 2𝑜) → 𝑘 ∈ 2𝑜)
72		xpscfv 16045	. . . . . . . . . 10 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝑘 ∈ 2𝑜) → (◡({𝑅} +𝑐 {𝑆})‘𝑘) = if(𝑘 = ∅, 𝑅, 𝑆))
73	69, 70, 71, 72	syl3anc 1318	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ 2𝑜) → (◡({𝑅} +𝑐 {𝑆})‘𝑘) = if(𝑘 = ∅, 𝑅, 𝑆))
74	73	fveq2d 6107	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ 2𝑜) → ( ·𝑠 ‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)) = ( ·𝑠 ‘if(𝑘 = ∅, 𝑅, 𝑆)))
75		eqidd 2611	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ 2𝑜) → 𝐴 = 𝐴)
76	3	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ 2𝑜) → 𝐵 ∈ 𝑋)
77	4	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ 2𝑜) → 𝐶 ∈ 𝑌)
78		xpscfv 16045	. . . . . . . . 9 ⊢ ((𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑌 ∧ 𝑘 ∈ 2𝑜) → (◡({𝐵} +𝑐 {𝐶})‘𝑘) = if(𝑘 = ∅, 𝐵, 𝐶))
79	76, 77, 71, 78	syl3anc 1318	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ 2𝑜) → (◡({𝐵} +𝑐 {𝐶})‘𝑘) = if(𝑘 = ∅, 𝐵, 𝐶))
80	74, 75, 79	oveq123d 6570	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ 2𝑜) → (𝐴( ·𝑠 ‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐵} +𝑐 {𝐶})‘𝑘)) = (𝐴( ·𝑠 ‘if(𝑘 = ∅, 𝑅, 𝑆))if(𝑘 = ∅, 𝐵, 𝐶)))
81		xpsvsca.6	. . . . . . . . 9 ⊢ (𝜑 → (𝐴 · 𝐵) ∈ 𝑋)
82	81	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ 2𝑜) → (𝐴 · 𝐵) ∈ 𝑋)
83		xpsvsca.7	. . . . . . . . 9 ⊢ (𝜑 → (𝐴 × 𝐶) ∈ 𝑌)
84	83	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ 2𝑜) → (𝐴 × 𝐶) ∈ 𝑌)
85		xpscfv 16045	. . . . . . . 8 ⊢ (((𝐴 · 𝐵) ∈ 𝑋 ∧ (𝐴 × 𝐶) ∈ 𝑌 ∧ 𝑘 ∈ 2𝑜) → (◡({(𝐴 · 𝐵)} +𝑐 {(𝐴 × 𝐶)})‘𝑘) = if(𝑘 = ∅, (𝐴 · 𝐵), (𝐴 × 𝐶)))
86	82, 84, 71, 85	syl3anc 1318	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ 2𝑜) → (◡({(𝐴 · 𝐵)} +𝑐 {(𝐴 × 𝐶)})‘𝑘) = if(𝑘 = ∅, (𝐴 · 𝐵), (𝐴 × 𝐶)))
87	68, 80, 86	3eqtr4a 2670	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ 2𝑜) → (𝐴( ·𝑠 ‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐵} +𝑐 {𝐶})‘𝑘)) = (◡({(𝐴 · 𝐵)} +𝑐 {(𝐴 × 𝐶)})‘𝑘))
88	87	mpteq2dva 4672	. . . . 5 ⊢ (𝜑 → (𝑘 ∈ 2𝑜 ↦ (𝐴( ·𝑠 ‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐵} +𝑐 {𝐶})‘𝑘))) = (𝑘 ∈ 2𝑜 ↦ (◡({(𝐴 · 𝐵)} +𝑐 {(𝐴 × 𝐶)})‘𝑘)))
89		eqid 2610	. . . . . 6 ⊢ (Base‘(𝐺Xs◡({𝑅} +𝑐 {𝑆}))) = (Base‘(𝐺Xs◡({𝑅} +𝑐 {𝑆})))
90	33	a1i 11	. . . . . 6 ⊢ (𝜑 → 𝐺 ∈ V)
91		2on 7455	. . . . . . 7 ⊢ 2𝑜 ∈ On
92	91	a1i 11	. . . . . 6 ⊢ (𝜑 → 2𝑜 ∈ On)
93		xpscfn 16042	. . . . . . 7 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊) → ◡({𝑅} +𝑐 {𝑆}) Fn 2𝑜)
94	20, 21, 93	syl2anc 691	. . . . . 6 ⊢ (𝜑 → ◡({𝑅} +𝑐 {𝑆}) Fn 2𝑜)
95	16, 25	eleqtrd 2690	. . . . . 6 ⊢ (𝜑 → ◡({𝐵} +𝑐 {𝐶}) ∈ (Base‘(𝐺Xs◡({𝑅} +𝑐 {𝑆}))))
96	23, 89, 41, 40, 90, 92, 94, 1, 95	prdsvscaval 15962	. . . . 5 ⊢ (𝜑 → (𝐴( ·𝑠 ‘(𝐺Xs◡({𝑅} +𝑐 {𝑆})))◡({𝐵} +𝑐 {𝐶})) = (𝑘 ∈ 2𝑜 ↦ (𝐴( ·𝑠 ‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐵} +𝑐 {𝐶})‘𝑘))))
97		xpscfn 16042	. . . . . . 7 ⊢ (((𝐴 · 𝐵) ∈ 𝑋 ∧ (𝐴 × 𝐶) ∈ 𝑌) → ◡({(𝐴 · 𝐵)} +𝑐 {(𝐴 × 𝐶)}) Fn 2𝑜)
98	81, 83, 97	syl2anc 691	. . . . . 6 ⊢ (𝜑 → ◡({(𝐴 · 𝐵)} +𝑐 {(𝐴 × 𝐶)}) Fn 2𝑜)
99		dffn5 6151	. . . . . 6 ⊢ (◡({(𝐴 · 𝐵)} +𝑐 {(𝐴 × 𝐶)}) Fn 2𝑜 ↔ ◡({(𝐴 · 𝐵)} +𝑐 {(𝐴 × 𝐶)}) = (𝑘 ∈ 2𝑜 ↦ (◡({(𝐴 · 𝐵)} +𝑐 {(𝐴 × 𝐶)})‘𝑘)))
100	98, 99	sylib 207	. . . . 5 ⊢ (𝜑 → ◡({(𝐴 · 𝐵)} +𝑐 {(𝐴 × 𝐶)}) = (𝑘 ∈ 2𝑜 ↦ (◡({(𝐴 · 𝐵)} +𝑐 {(𝐴 × 𝐶)})‘𝑘)))
101	88, 96, 100	3eqtr4d 2654	. . . 4 ⊢ (𝜑 → (𝐴( ·𝑠 ‘(𝐺Xs◡({𝑅} +𝑐 {𝑆})))◡({𝐵} +𝑐 {𝐶})) = ◡({(𝐴 · 𝐵)} +𝑐 {(𝐴 × 𝐶)}))
102	101	fveq2d 6107	. . 3 ⊢ (𝜑 → (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘(𝐴( ·𝑠 ‘(𝐺Xs◡({𝑅} +𝑐 {𝑆})))◡({𝐵} +𝑐 {𝐶}))) = (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘◡({(𝐴 · 𝐵)} +𝑐 {(𝐴 × 𝐶)})))
103		df-ov 6552	. . . . 5 ⊢ ((𝐴 · 𝐵)(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))(𝐴 × 𝐶)) = ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘⟨(𝐴 · 𝐵), (𝐴 × 𝐶)⟩)
104	5	xpsfval 16050	. . . . . 6 ⊢ (((𝐴 · 𝐵) ∈ 𝑋 ∧ (𝐴 × 𝐶) ∈ 𝑌) → ((𝐴 · 𝐵)(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))(𝐴 × 𝐶)) = ◡({(𝐴 · 𝐵)} +𝑐 {(𝐴 × 𝐶)}))
105	81, 83, 104	syl2anc 691	. . . . 5 ⊢ (𝜑 → ((𝐴 · 𝐵)(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))(𝐴 × 𝐶)) = ◡({(𝐴 · 𝐵)} +𝑐 {(𝐴 × 𝐶)}))
106	103, 105	syl5eqr 2658	. . . 4 ⊢ (𝜑 → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘⟨(𝐴 · 𝐵), (𝐴 × 𝐶)⟩) = ◡({(𝐴 · 𝐵)} +𝑐 {(𝐴 × 𝐶)}))
107		opelxpi 5072	. . . . . 6 ⊢ (((𝐴 · 𝐵) ∈ 𝑋 ∧ (𝐴 × 𝐶) ∈ 𝑌) → ⟨(𝐴 · 𝐵), (𝐴 × 𝐶)⟩ ∈ (𝑋 × 𝑌))
108	81, 83, 107	syl2anc 691	. . . . 5 ⊢ (𝜑 → ⟨(𝐴 · 𝐵), (𝐴 × 𝐶)⟩ ∈ (𝑋 × 𝑌))
109		f1ocnvfv 6434	. . . . 5 ⊢ (((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})):(𝑋 × 𝑌)–1-1-onto→ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) ∧ ⟨(𝐴 · 𝐵), (𝐴 × 𝐶)⟩ ∈ (𝑋 × 𝑌)) → (((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘⟨(𝐴 · 𝐵), (𝐴 × 𝐶)⟩) = ◡({(𝐴 · 𝐵)} +𝑐 {(𝐴 × 𝐶)}) → (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘◡({(𝐴 · 𝐵)} +𝑐 {(𝐴 × 𝐶)})) = ⟨(𝐴 · 𝐵), (𝐴 × 𝐶)⟩))
110	11, 108, 109	sylancr 694	. . . 4 ⊢ (𝜑 → (((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘⟨(𝐴 · 𝐵), (𝐴 × 𝐶)⟩) = ◡({(𝐴 · 𝐵)} +𝑐 {(𝐴 × 𝐶)}) → (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘◡({(𝐴 · 𝐵)} +𝑐 {(𝐴 × 𝐶)})) = ⟨(𝐴 · 𝐵), (𝐴 × 𝐶)⟩))
111	106, 110	mpd 15	. . 3 ⊢ (𝜑 → (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘◡({(𝐴 · 𝐵)} +𝑐 {(𝐴 × 𝐶)})) = ⟨(𝐴 · 𝐵), (𝐴 × 𝐶)⟩)
112	102, 111	eqtrd 2644	. 2 ⊢ (𝜑 → (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘(𝐴( ·𝑠 ‘(𝐺Xs◡({𝑅} +𝑐 {𝑆})))◡({𝐵} +𝑐 {𝐶}))) = ⟨(𝐴 · 𝐵), (𝐴 × 𝐶)⟩)
113	45, 49, 112	3eqtr3d 2652	1 ⊢ (𝜑 → (𝐴 ∙ ⟨𝐵, 𝐶⟩) = ⟨(𝐴 · 𝐵), (𝐴 × 𝐶)⟩)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 383   = wceq 1475  ⊤wtru 1476   ∈ wcel 1977  Vcvv 3173  ∅c0 3874  ifcif 4036  {csn 4125  ⟨cop 4131   ↦ cmpt 4643   × cxp 5036  ^◡ccnv 5037  ran crn 5039  Oncon0 5640   Fn wfn 5799  ⟶wf 5800  –onto→wfo 5802  –1-1-onto→wf1o 5803  ‘cfv 5804  (class class class)co 6549   ↦ cmpt2 6551  2_𝑜c2o 7441   +_𝑐 ccda 8872  Basecbs 15695  Scalarcsca 15771   ·_𝑠 cvsca 15772  X_scprds 15929   ×_s cxps 15989

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-1st 7059  df-2nd 7060  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-2o 7448  df-oadd 7451  df-er 7629  df-map 7746  df-ixp 7795  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-sup 8231  df-inf 8232  df-cda 8873  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-nn 10898  df-2 10956  df-3 10957  df-4 10958  df-5 10959  df-6 10960  df-7 10961  df-8 10962  df-9 10963  df-n0 11170  df-z 11255  df-dec 11370  df-uz 11564  df-fz 12198  df-struct 15697  df-ndx 15698  df-slot 15699  df-base 15700  df-plusg 15781  df-mulr 15782  df-sca 15784  df-vsca 15785  df-ip 15786  df-tset 15787  df-ple 15788  df-ds 15791  df-hom 15793  df-cco 15794  df-prds 15931  df-imas 15991  df-xps 15993

This theorem is referenced by: (None)