Theorem xpsaddlem 16058

Description: Lemma for xpsadd 16059 and xpsmul 16060. (Contributed by Mario Carneiro, 15-Aug-2015.)

Hypotheses

Ref	Expression
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	⊢ 𝐹 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))
xpsaddlem.u	⊢ 𝑈 = ((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆}))
xpsaddlem.1	⊢ ((𝜑 ∧ ◡({𝐴} +𝑐 {𝐵}) ∈ ran 𝐹 ∧ ◡({𝐶} +𝑐 {𝐷}) ∈ ran 𝐹) → ((◡𝐹‘◡({𝐴} +𝑐 {𝐵})) ∙ (◡𝐹‘◡({𝐶} +𝑐 {𝐷}))) = (◡𝐹‘(◡({𝐴} +𝑐 {𝐵})(𝐸‘𝑈)◡({𝐶} +𝑐 {𝐷}))))
xpsaddlem.2	⊢ ((◡({𝑅} +𝑐 {𝑆}) Fn 2𝑜 ∧ ◡({𝐴} +𝑐 {𝐵}) ∈ (Base‘𝑈) ∧ ◡({𝐶} +𝑐 {𝐷}) ∈ (Base‘𝑈)) → (◡({𝐴} +𝑐 {𝐵})(𝐸‘𝑈)◡({𝐶} +𝑐 {𝐷})) = (𝑘 ∈ 2𝑜 ↦ ((◡({𝐴} +𝑐 {𝐵})‘𝑘)(𝐸‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐶} +𝑐 {𝐷})‘𝑘))))

Assertion

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

Distinct variable groups:   𝑥,𝑘,𝑦,𝐴   𝐵,𝑘,𝑥,𝑦   𝐶,𝑘,𝑥,𝑦   𝐷,𝑘,𝑥,𝑦   𝑆,𝑘   𝑈,𝑘   𝑥,𝑊   𝜑,𝑘   · ,𝑘,𝑥,𝑦   × ,𝑘,𝑥,𝑦   𝑘,𝑋,𝑥,𝑦   𝑅,𝑘,𝑥   𝑘,𝑌,𝑥,𝑦

Allowed substitution hints:   𝜑(𝑥,𝑦)   𝑅(𝑦)   𝑆(𝑥,𝑦)   ∙ (𝑥,𝑦,𝑘)   𝑇(𝑥,𝑦,𝑘)   𝑈(𝑥,𝑦)   𝐸(𝑥,𝑦,𝑘)   𝐹(𝑥,𝑦,𝑘)   𝑉(𝑥,𝑦,𝑘)   𝑊(𝑦,𝑘)

Proof of Theorem xpsaddlem

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 383   ∧ w3a 1031   = wceq 1475   ∈ wcel 1977  ∅c0 3874  ifcif 4036  {csn 4125  ⟨cop 4131   ↦ cmpt 4643   × cxp 5036  ^◡ccnv 5037  ran crn 5039   Fn wfn 5799  ⟶wf 5800  –1-1-onto→wf1o 5803  ‘cfv 5804  (class class class)co 6549   ↦ cmpt2 6551  2_𝑜c2o 7441   +_𝑐 ccda 8872  Basecbs 15695  Scalarcsca 15771  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-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

This theorem is referenced by:  xpsadd  16059  xpsmul  16060