Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  xpsvsca Structured version   Visualization version   GIF version

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.
StepHypRef Expression
1 xpsvsca.3 . . 3 (𝜑𝐴𝐾)
2 df-ov 6552 . . . . 5 (𝐵(𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦}))𝐶) = ((𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦}))‘⟨𝐵, 𝐶⟩)
3 xpsvsca.4 . . . . . 6 (𝜑𝐵𝑋)
4 xpsvsca.5 . . . . . 6 (𝜑𝐶𝑌)
5 eqid 2610 . . . . . . 7 (𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦})) = (𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦}))
65xpsfval 16050 . . . . . 6 ((𝐵𝑋𝐶𝑌) → (𝐵(𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦}))𝐶) = ({𝐵} +𝑐 {𝐶}))
73, 4, 6syl2anc 691 . . . . 5 (𝜑 → (𝐵(𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦}))𝐶) = ({𝐵} +𝑐 {𝐶}))
82, 7syl5eqr 2658 . . . 4 (𝜑 → ((𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦}))‘⟨𝐵, 𝐶⟩) = ({𝐵} +𝑐 {𝐶}))
9 opelxpi 5072 . . . . . 6 ((𝐵𝑋𝐶𝑌) → ⟨𝐵, 𝐶⟩ ∈ (𝑋 × 𝑌))
103, 4, 9syl2anc 691 . . . . 5 (𝜑 → ⟨𝐵, 𝐶⟩ ∈ (𝑋 × 𝑌))
115xpsff1o2 16054 . . . . . . 7 (𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦})):(𝑋 × 𝑌)–1-1-onto→ran (𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦}))
12 f1of 6050 . . . . . . 7 ((𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦})):(𝑋 × 𝑌)–1-1-onto→ran (𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦})) → (𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦})):(𝑋 × 𝑌)⟶ran (𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦})))
1311, 12ax-mp 5 . . . . . 6 (𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦})):(𝑋 × 𝑌)⟶ran (𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦}))
1413ffvelrni 6266 . . . . 5 (⟨𝐵, 𝐶⟩ ∈ (𝑋 × 𝑌) → ((𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦}))‘⟨𝐵, 𝐶⟩) ∈ ran (𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦})))
1510, 14syl 17 . . . 4 (𝜑 → ((𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦}))‘⟨𝐵, 𝐶⟩) ∈ ran (𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦})))
168, 15eqeltrrd 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({𝑅} +𝑐 {𝑆}))
2417, 18, 19, 20, 21, 5, 22, 23xpsval 16055 . . . 4 (𝜑𝑇 = ((𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦})) “s (𝐺Xs({𝑅} +𝑐 {𝑆}))))
2517, 18, 19, 20, 21, 5, 22, 23xpslem 16056 . . . 4 (𝜑 → ran (𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦})) = (Base‘(𝐺Xs({𝑅} +𝑐 {𝑆}))))
26 f1ocnv 6062 . . . . . 6 ((𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦})):(𝑋 × 𝑌)–1-1-onto→ran (𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦})) → (𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦})):ran (𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦}))–1-1-onto→(𝑋 × 𝑌))
2711, 26mp1i 13 . . . . 5 (𝜑(𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦})):ran (𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦}))–1-1-onto→(𝑋 × 𝑌))
28 f1ofo 6057 . . . . 5 ((𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦})):ran (𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦}))–1-1-onto→(𝑋 × 𝑌) → (𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦})):ran (𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦}))–onto→(𝑋 × 𝑌))
2927, 28syl 17 . . . 4 (𝜑(𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦})):ran (𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦}))–onto→(𝑋 × 𝑌))
30 ovex 6577 . . . . 5 (𝐺Xs({𝑅} +𝑐 {𝑆})) ∈ V
3130a1i 11 . . . 4 (𝜑 → (𝐺Xs({𝑅} +𝑐 {𝑆})) ∈ V)
32 fvex 6113 . . . . . . . 8 (Scalar‘𝑅) ∈ V
3322, 32eqeltri 2684 . . . . . . 7 𝐺 ∈ V
3433a1i 11 . . . . . 6 (⊤ → 𝐺 ∈ V)
35 ovex 6577 . . . . . . . 8 ({𝑅} +𝑐 {𝑆}) ∈ V
3635cnvex 7006 . . . . . . 7 ({𝑅} +𝑐 {𝑆}) ∈ V
3736a1i 11 . . . . . 6 (⊤ → ({𝑅} +𝑐 {𝑆}) ∈ V)
3823, 34, 37prdssca 15939 . . . . 5 (⊤ → 𝐺 = (Scalar‘(𝐺Xs({𝑅} +𝑐 {𝑆}))))
3938trud 1484 . . . 4 𝐺 = (Scalar‘(𝐺Xs({𝑅} +𝑐 {𝑆})))
40 xpsvsca.k . . . 4 𝐾 = (Base‘𝐺)
41 eqid 2610 . . . 4 ( ·𝑠 ‘(𝐺Xs({𝑅} +𝑐 {𝑆}))) = ( ·𝑠 ‘(𝐺Xs({𝑅} +𝑐 {𝑆})))
42 xpsvsca.p . . . 4 = ( ·𝑠𝑇)
4327f1ovscpbl 16009 . . . 4 ((𝜑 ∧ (𝑎𝐾𝑏 ∈ ran (𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦})) ∧ 𝑐 ∈ ran (𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦})))) → (((𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦}))‘𝑏) = ((𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦}))‘𝑐) → ((𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦}))‘(𝑎( ·𝑠 ‘(𝐺Xs({𝑅} +𝑐 {𝑆})))𝑏)) = ((𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦}))‘(𝑎( ·𝑠 ‘(𝐺Xs({𝑅} +𝑐 {𝑆})))𝑐))))
4424, 25, 29, 31, 39, 40, 41, 42, 43imasvscaval 16021 . . 3 ((𝜑𝐴𝐾({𝐵} +𝑐 {𝐶}) ∈ ran (𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦}))) → (𝐴 ((𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦}))‘({𝐵} +𝑐 {𝐶}))) = ((𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦}))‘(𝐴( ·𝑠 ‘(𝐺Xs({𝑅} +𝑐 {𝑆})))({𝐵} +𝑐 {𝐶}))))
451, 16, 44mpd3an23 1418 . 2 (𝜑 → (𝐴 ((𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦}))‘({𝐵} +𝑐 {𝐶}))) = ((𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦}))‘(𝐴( ·𝑠 ‘(𝐺Xs({𝑅} +𝑐 {𝑆})))({𝐵} +𝑐 {𝐶}))))
46 f1ocnvfv 6434 . . . . 5 (((𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦})):(𝑋 × 𝑌)–1-1-onto→ran (𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦})) ∧ ⟨𝐵, 𝐶⟩ ∈ (𝑋 × 𝑌)) → (((𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦}))‘⟨𝐵, 𝐶⟩) = ({𝐵} +𝑐 {𝐶}) → ((𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦}))‘({𝐵} +𝑐 {𝐶})) = ⟨𝐵, 𝐶⟩))
4711, 10, 46sylancr 694 . . . 4 (𝜑 → (((𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦}))‘⟨𝐵, 𝐶⟩) = ({𝐵} +𝑐 {𝐶}) → ((𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦}))‘({𝐵} +𝑐 {𝐶})) = ⟨𝐵, 𝐶⟩))
488, 47mpd 15 . . 3 (𝜑 → ((𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦}))‘({𝐵} +𝑐 {𝐶})) = ⟨𝐵, 𝐶⟩)
4948oveq2d 6565 . 2 (𝜑 → (𝐴 ((𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦}))‘({𝐵} +𝑐 {𝐶}))) = (𝐴 𝐵, 𝐶⟩))
50 iftrue 4042 . . . . . . . . . . . 12 (𝑘 = ∅ → if(𝑘 = ∅, 𝑅, 𝑆) = 𝑅)
5150fveq2d 6107 . . . . . . . . . . 11 (𝑘 = ∅ → ( ·𝑠 ‘if(𝑘 = ∅, 𝑅, 𝑆)) = ( ·𝑠𝑅))
52 xpsvsca.m . . . . . . . . . . 11 · = ( ·𝑠𝑅)
5351, 52syl6eqr 2662 . . . . . . . . . 10 (𝑘 = ∅ → ( ·𝑠 ‘if(𝑘 = ∅, 𝑅, 𝑆)) = · )
54 eqidd 2611 . . . . . . . . . 10 (𝑘 = ∅ → 𝐴 = 𝐴)
55 iftrue 4042 . . . . . . . . . 10 (𝑘 = ∅ → if(𝑘 = ∅, 𝐵, 𝐶) = 𝐵)
5653, 54, 55oveq123d 6570 . . . . . . . . 9 (𝑘 = ∅ → (𝐴( ·𝑠 ‘if(𝑘 = ∅, 𝑅, 𝑆))if(𝑘 = ∅, 𝐵, 𝐶)) = (𝐴 · 𝐵))
57 iftrue 4042 . . . . . . . . 9 (𝑘 = ∅ → if(𝑘 = ∅, (𝐴 · 𝐵), (𝐴 × 𝐶)) = (𝐴 · 𝐵))
5856, 57eqtr4d 2647 . . . . . . . 8 (𝑘 = ∅ → (𝐴( ·𝑠 ‘if(𝑘 = ∅, 𝑅, 𝑆))if(𝑘 = ∅, 𝐵, 𝐶)) = if(𝑘 = ∅, (𝐴 · 𝐵), (𝐴 × 𝐶)))
59 iffalse 4045 . . . . . . . . . . . 12 𝑘 = ∅ → if(𝑘 = ∅, 𝑅, 𝑆) = 𝑆)
6059fveq2d 6107 . . . . . . . . . . 11 𝑘 = ∅ → ( ·𝑠 ‘if(𝑘 = ∅, 𝑅, 𝑆)) = ( ·𝑠𝑆))
61 xpsvsca.n . . . . . . . . . . 11 × = ( ·𝑠𝑆)
6260, 61syl6eqr 2662 . . . . . . . . . 10 𝑘 = ∅ → ( ·𝑠 ‘if(𝑘 = ∅, 𝑅, 𝑆)) = × )
63 eqidd 2611 . . . . . . . . . 10 𝑘 = ∅ → 𝐴 = 𝐴)
64 iffalse 4045 . . . . . . . . . 10 𝑘 = ∅ → if(𝑘 = ∅, 𝐵, 𝐶) = 𝐶)
6562, 63, 64oveq123d 6570 . . . . . . . . 9 𝑘 = ∅ → (𝐴( ·𝑠 ‘if(𝑘 = ∅, 𝑅, 𝑆))if(𝑘 = ∅, 𝐵, 𝐶)) = (𝐴 × 𝐶))
66 iffalse 4045 . . . . . . . . 9 𝑘 = ∅ → if(𝑘 = ∅, (𝐴 · 𝐵), (𝐴 × 𝐶)) = (𝐴 × 𝐶))
6765, 66eqtr4d 2647 . . . . . . . 8 𝑘 = ∅ → (𝐴( ·𝑠 ‘if(𝑘 = ∅, 𝑅, 𝑆))if(𝑘 = ∅, 𝐵, 𝐶)) = if(𝑘 = ∅, (𝐴 · 𝐵), (𝐴 × 𝐶)))
6858, 67pm2.61i 175 . . . . . . 7 (𝐴( ·𝑠 ‘if(𝑘 = ∅, 𝑅, 𝑆))if(𝑘 = ∅, 𝐵, 𝐶)) = if(𝑘 = ∅, (𝐴 · 𝐵), (𝐴 × 𝐶))
6920adantr 480 . . . . . . . . . 10 ((𝜑𝑘 ∈ 2𝑜) → 𝑅𝑉)
7021adantr 480 . . . . . . . . . 10 ((𝜑𝑘 ∈ 2𝑜) → 𝑆𝑊)
71 simpr 476 . . . . . . . . . 10 ((𝜑𝑘 ∈ 2𝑜) → 𝑘 ∈ 2𝑜)
72 xpscfv 16045 . . . . . . . . . 10 ((𝑅𝑉𝑆𝑊𝑘 ∈ 2𝑜) → (({𝑅} +𝑐 {𝑆})‘𝑘) = if(𝑘 = ∅, 𝑅, 𝑆))
7369, 70, 71, 72syl3anc 1318 . . . . . . . . 9 ((𝜑𝑘 ∈ 2𝑜) → (({𝑅} +𝑐 {𝑆})‘𝑘) = if(𝑘 = ∅, 𝑅, 𝑆))
7473fveq2d 6107 . . . . . . . 8 ((𝜑𝑘 ∈ 2𝑜) → ( ·𝑠 ‘(({𝑅} +𝑐 {𝑆})‘𝑘)) = ( ·𝑠 ‘if(𝑘 = ∅, 𝑅, 𝑆)))
75 eqidd 2611 . . . . . . . 8 ((𝜑𝑘 ∈ 2𝑜) → 𝐴 = 𝐴)
763adantr 480 . . . . . . . . 9 ((𝜑𝑘 ∈ 2𝑜) → 𝐵𝑋)
774adantr 480 . . . . . . . . 9 ((𝜑𝑘 ∈ 2𝑜) → 𝐶𝑌)
78 xpscfv 16045 . . . . . . . . 9 ((𝐵𝑋𝐶𝑌𝑘 ∈ 2𝑜) → (({𝐵} +𝑐 {𝐶})‘𝑘) = if(𝑘 = ∅, 𝐵, 𝐶))
7976, 77, 71, 78syl3anc 1318 . . . . . . . 8 ((𝜑𝑘 ∈ 2𝑜) → (({𝐵} +𝑐 {𝐶})‘𝑘) = if(𝑘 = ∅, 𝐵, 𝐶))
8074, 75, 79oveq123d 6570 . . . . . . 7 ((𝜑𝑘 ∈ 2𝑜) → (𝐴( ·𝑠 ‘(({𝑅} +𝑐 {𝑆})‘𝑘))(({𝐵} +𝑐 {𝐶})‘𝑘)) = (𝐴( ·𝑠 ‘if(𝑘 = ∅, 𝑅, 𝑆))if(𝑘 = ∅, 𝐵, 𝐶)))
81 xpsvsca.6 . . . . . . . . 9 (𝜑 → (𝐴 · 𝐵) ∈ 𝑋)
8281adantr 480 . . . . . . . 8 ((𝜑𝑘 ∈ 2𝑜) → (𝐴 · 𝐵) ∈ 𝑋)
83 xpsvsca.7 . . . . . . . . 9 (𝜑 → (𝐴 × 𝐶) ∈ 𝑌)
8483adantr 480 . . . . . . . 8 ((𝜑𝑘 ∈ 2𝑜) → (𝐴 × 𝐶) ∈ 𝑌)
85 xpscfv 16045 . . . . . . . 8 (((𝐴 · 𝐵) ∈ 𝑋 ∧ (𝐴 × 𝐶) ∈ 𝑌𝑘 ∈ 2𝑜) → (({(𝐴 · 𝐵)} +𝑐 {(𝐴 × 𝐶)})‘𝑘) = if(𝑘 = ∅, (𝐴 · 𝐵), (𝐴 × 𝐶)))
8682, 84, 71, 85syl3anc 1318 . . . . . . 7 ((𝜑𝑘 ∈ 2𝑜) → (({(𝐴 · 𝐵)} +𝑐 {(𝐴 × 𝐶)})‘𝑘) = if(𝑘 = ∅, (𝐴 · 𝐵), (𝐴 × 𝐶)))
8768, 80, 863eqtr4a 2670 . . . . . 6 ((𝜑𝑘 ∈ 2𝑜) → (𝐴( ·𝑠 ‘(({𝑅} +𝑐 {𝑆})‘𝑘))(({𝐵} +𝑐 {𝐶})‘𝑘)) = (({(𝐴 · 𝐵)} +𝑐 {(𝐴 × 𝐶)})‘𝑘))
8887mpteq2dva 4672 . . . . 5 (𝜑 → (𝑘 ∈ 2𝑜 ↦ (𝐴( ·𝑠 ‘(({𝑅} +𝑐 {𝑆})‘𝑘))(({𝐵} +𝑐 {𝐶})‘𝑘))) = (𝑘 ∈ 2𝑜 ↦ (({(𝐴 · 𝐵)} +𝑐 {(𝐴 × 𝐶)})‘𝑘)))
89 eqid 2610 . . . . . 6 (Base‘(𝐺Xs({𝑅} +𝑐 {𝑆}))) = (Base‘(𝐺Xs({𝑅} +𝑐 {𝑆})))
9033a1i 11 . . . . . 6 (𝜑𝐺 ∈ V)
91 2on 7455 . . . . . . 7 2𝑜 ∈ On
9291a1i 11 . . . . . 6 (𝜑 → 2𝑜 ∈ On)
93 xpscfn 16042 . . . . . . 7 ((𝑅𝑉𝑆𝑊) → ({𝑅} +𝑐 {𝑆}) Fn 2𝑜)
9420, 21, 93syl2anc 691 . . . . . 6 (𝜑({𝑅} +𝑐 {𝑆}) Fn 2𝑜)
9516, 25eleqtrd 2690 . . . . . 6 (𝜑({𝐵} +𝑐 {𝐶}) ∈ (Base‘(𝐺Xs({𝑅} +𝑐 {𝑆}))))
9623, 89, 41, 40, 90, 92, 94, 1, 95prdsvscaval 15962 . . . . 5 (𝜑 → (𝐴( ·𝑠 ‘(𝐺Xs({𝑅} +𝑐 {𝑆})))({𝐵} +𝑐 {𝐶})) = (𝑘 ∈ 2𝑜 ↦ (𝐴( ·𝑠 ‘(({𝑅} +𝑐 {𝑆})‘𝑘))(({𝐵} +𝑐 {𝐶})‘𝑘))))
97 xpscfn 16042 . . . . . . 7 (((𝐴 · 𝐵) ∈ 𝑋 ∧ (𝐴 × 𝐶) ∈ 𝑌) → ({(𝐴 · 𝐵)} +𝑐 {(𝐴 × 𝐶)}) Fn 2𝑜)
9881, 83, 97syl2anc 691 . . . . . 6 (𝜑({(𝐴 · 𝐵)} +𝑐 {(𝐴 × 𝐶)}) Fn 2𝑜)
99 dffn5 6151 . . . . . 6 (({(𝐴 · 𝐵)} +𝑐 {(𝐴 × 𝐶)}) Fn 2𝑜({(𝐴 · 𝐵)} +𝑐 {(𝐴 × 𝐶)}) = (𝑘 ∈ 2𝑜 ↦ (({(𝐴 · 𝐵)} +𝑐 {(𝐴 × 𝐶)})‘𝑘)))
10098, 99sylib 207 . . . . 5 (𝜑({(𝐴 · 𝐵)} +𝑐 {(𝐴 × 𝐶)}) = (𝑘 ∈ 2𝑜 ↦ (({(𝐴 · 𝐵)} +𝑐 {(𝐴 × 𝐶)})‘𝑘)))
10188, 96, 1003eqtr4d 2654 . . . 4 (𝜑 → (𝐴( ·𝑠 ‘(𝐺Xs({𝑅} +𝑐 {𝑆})))({𝐵} +𝑐 {𝐶})) = ({(𝐴 · 𝐵)} +𝑐 {(𝐴 × 𝐶)}))
102101fveq2d 6107 . . 3 (𝜑 → ((𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦}))‘(𝐴( ·𝑠 ‘(𝐺Xs({𝑅} +𝑐 {𝑆})))({𝐵} +𝑐 {𝐶}))) = ((𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦}))‘({(𝐴 · 𝐵)} +𝑐 {(𝐴 × 𝐶)})))
103 df-ov 6552 . . . . 5 ((𝐴 · 𝐵)(𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦}))(𝐴 × 𝐶)) = ((𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦}))‘⟨(𝐴 · 𝐵), (𝐴 × 𝐶)⟩)
1045xpsfval 16050 . . . . . 6 (((𝐴 · 𝐵) ∈ 𝑋 ∧ (𝐴 × 𝐶) ∈ 𝑌) → ((𝐴 · 𝐵)(𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦}))(𝐴 × 𝐶)) = ({(𝐴 · 𝐵)} +𝑐 {(𝐴 × 𝐶)}))
10581, 83, 104syl2anc 691 . . . . 5 (𝜑 → ((𝐴 · 𝐵)(𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦}))(𝐴 × 𝐶)) = ({(𝐴 · 𝐵)} +𝑐 {(𝐴 × 𝐶)}))
106103, 105syl5eqr 2658 . . . 4 (𝜑 → ((𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦}))‘⟨(𝐴 · 𝐵), (𝐴 × 𝐶)⟩) = ({(𝐴 · 𝐵)} +𝑐 {(𝐴 × 𝐶)}))
107 opelxpi 5072 . . . . . 6 (((𝐴 · 𝐵) ∈ 𝑋 ∧ (𝐴 × 𝐶) ∈ 𝑌) → ⟨(𝐴 · 𝐵), (𝐴 × 𝐶)⟩ ∈ (𝑋 × 𝑌))
10881, 83, 107syl2anc 691 . . . . 5 (𝜑 → ⟨(𝐴 · 𝐵), (𝐴 × 𝐶)⟩ ∈ (𝑋 × 𝑌))
109 f1ocnvfv 6434 . . . . 5 (((𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦})):(𝑋 × 𝑌)–1-1-onto→ran (𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦})) ∧ ⟨(𝐴 · 𝐵), (𝐴 × 𝐶)⟩ ∈ (𝑋 × 𝑌)) → (((𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦}))‘⟨(𝐴 · 𝐵), (𝐴 × 𝐶)⟩) = ({(𝐴 · 𝐵)} +𝑐 {(𝐴 × 𝐶)}) → ((𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦}))‘({(𝐴 · 𝐵)} +𝑐 {(𝐴 × 𝐶)})) = ⟨(𝐴 · 𝐵), (𝐴 × 𝐶)⟩))
11011, 108, 109sylancr 694 . . . 4 (𝜑 → (((𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦}))‘⟨(𝐴 · 𝐵), (𝐴 × 𝐶)⟩) = ({(𝐴 · 𝐵)} +𝑐 {(𝐴 × 𝐶)}) → ((𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦}))‘({(𝐴 · 𝐵)} +𝑐 {(𝐴 × 𝐶)})) = ⟨(𝐴 · 𝐵), (𝐴 × 𝐶)⟩))
111106, 110mpd 15 . . 3 (𝜑 → ((𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦}))‘({(𝐴 · 𝐵)} +𝑐 {(𝐴 × 𝐶)})) = ⟨(𝐴 · 𝐵), (𝐴 × 𝐶)⟩)
112102, 111eqtrd 2644 . 2 (𝜑 → ((𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦}))‘(𝐴( ·𝑠 ‘(𝐺Xs({𝑅} +𝑐 {𝑆})))({𝐵} +𝑐 {𝐶}))) = ⟨(𝐴 · 𝐵), (𝐴 × 𝐶)⟩)
11345, 49, 1123eqtr3d 2652 1 (𝜑 → (𝐴 𝐵, 𝐶⟩) = ⟨(𝐴 · 𝐵), (𝐴 × 𝐶)⟩)
 Colors of variables: wff setvar class 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  Xscprds 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)
 Copyright terms: Public domain W3C validator