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

Theorem xpsvsca 17527
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 7414 . . . . 5 (𝐡(π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©})𝐢) = ((π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©})β€˜βŸ¨π΅, 𝐢⟩)
3 xpsvsca.4 . . . . . 6 (πœ‘ β†’ 𝐡 ∈ 𝑋)
4 xpsvsca.5 . . . . . 6 (πœ‘ β†’ 𝐢 ∈ π‘Œ)
5 eqid 2730 . . . . . . 7 (π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©}) = (π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©})
65xpsfval 17516 . . . . . 6 ((𝐡 ∈ 𝑋 ∧ 𝐢 ∈ π‘Œ) β†’ (𝐡(π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©})𝐢) = {βŸ¨βˆ…, 𝐡⟩, ⟨1o, 𝐢⟩})
73, 4, 6syl2anc 582 . . . . 5 (πœ‘ β†’ (𝐡(π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©})𝐢) = {βŸ¨βˆ…, 𝐡⟩, ⟨1o, 𝐢⟩})
82, 7eqtr3id 2784 . . . 4 (πœ‘ β†’ ((π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©})β€˜βŸ¨π΅, 𝐢⟩) = {βŸ¨βˆ…, 𝐡⟩, ⟨1o, 𝐢⟩})
93, 4opelxpd 5714 . . . . 5 (πœ‘ β†’ ⟨𝐡, 𝐢⟩ ∈ (𝑋 Γ— π‘Œ))
105xpsff1o2 17519 . . . . . . 7 (π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©}):(𝑋 Γ— π‘Œ)–1-1-ontoβ†’ran (π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©})
11 f1of 6832 . . . . . . 7 ((π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©}):(𝑋 Γ— π‘Œ)–1-1-ontoβ†’ran (π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©}) β†’ (π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©}):(𝑋 Γ— π‘Œ)⟢ran (π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©}))
1210, 11ax-mp 5 . . . . . 6 (π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©}):(𝑋 Γ— π‘Œ)⟢ran (π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©})
1312ffvelcdmi 7084 . . . . 5 (⟨𝐡, 𝐢⟩ ∈ (𝑋 Γ— π‘Œ) β†’ ((π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©})β€˜βŸ¨π΅, 𝐢⟩) ∈ ran (π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©}))
149, 13syl 17 . . . 4 (πœ‘ β†’ ((π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©})β€˜βŸ¨π΅, 𝐢⟩) ∈ ran (π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©}))
158, 14eqeltrrd 2832 . . 3 (πœ‘ β†’ {βŸ¨βˆ…, 𝐡⟩, ⟨1o, 𝐢⟩} ∈ ran (π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©}))
16 xpssca.t . . . . 5 𝑇 = (𝑅 Γ—s 𝑆)
17 xpsvsca.x . . . . 5 𝑋 = (Baseβ€˜π‘…)
18 xpsvsca.y . . . . 5 π‘Œ = (Baseβ€˜π‘†)
19 xpssca.1 . . . . 5 (πœ‘ β†’ 𝑅 ∈ 𝑉)
20 xpssca.2 . . . . 5 (πœ‘ β†’ 𝑆 ∈ π‘Š)
21 xpssca.g . . . . 5 𝐺 = (Scalarβ€˜π‘…)
22 eqid 2730 . . . . 5 (𝐺Xs{βŸ¨βˆ…, π‘…βŸ©, ⟨1o, π‘†βŸ©}) = (𝐺Xs{βŸ¨βˆ…, π‘…βŸ©, ⟨1o, π‘†βŸ©})
2316, 17, 18, 19, 20, 5, 21, 22xpsval 17520 . . . 4 (πœ‘ β†’ 𝑇 = (β—‘(π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©}) β€œs (𝐺Xs{βŸ¨βˆ…, π‘…βŸ©, ⟨1o, π‘†βŸ©})))
2416, 17, 18, 19, 20, 5, 21, 22xpsrnbas 17521 . . . 4 (πœ‘ β†’ ran (π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©}) = (Baseβ€˜(𝐺Xs{βŸ¨βˆ…, π‘…βŸ©, ⟨1o, π‘†βŸ©})))
25 f1ocnv 6844 . . . . . 6 ((π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©}):(𝑋 Γ— π‘Œ)–1-1-ontoβ†’ran (π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©}) β†’ β—‘(π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©}):ran (π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©})–1-1-ontoβ†’(𝑋 Γ— π‘Œ))
2610, 25mp1i 13 . . . . 5 (πœ‘ β†’ β—‘(π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©}):ran (π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©})–1-1-ontoβ†’(𝑋 Γ— π‘Œ))
27 f1ofo 6839 . . . . 5 (β—‘(π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©}):ran (π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©})–1-1-ontoβ†’(𝑋 Γ— π‘Œ) β†’ β—‘(π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©}):ran (π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©})–ontoβ†’(𝑋 Γ— π‘Œ))
2826, 27syl 17 . . . 4 (πœ‘ β†’ β—‘(π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©}):ran (π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©})–ontoβ†’(𝑋 Γ— π‘Œ))
29 ovexd 7446 . . . 4 (πœ‘ β†’ (𝐺Xs{βŸ¨βˆ…, π‘…βŸ©, ⟨1o, π‘†βŸ©}) ∈ V)
3021fvexi 6904 . . . . . . 7 𝐺 ∈ V
3130a1i 11 . . . . . 6 (⊀ β†’ 𝐺 ∈ V)
32 prex 5431 . . . . . . 7 {βŸ¨βˆ…, π‘…βŸ©, ⟨1o, π‘†βŸ©} ∈ V
3332a1i 11 . . . . . 6 (⊀ β†’ {βŸ¨βˆ…, π‘…βŸ©, ⟨1o, π‘†βŸ©} ∈ V)
3422, 31, 33prdssca 17406 . . . . 5 (⊀ β†’ 𝐺 = (Scalarβ€˜(𝐺Xs{βŸ¨βˆ…, π‘…βŸ©, ⟨1o, π‘†βŸ©})))
3534mptru 1546 . . . 4 𝐺 = (Scalarβ€˜(𝐺Xs{βŸ¨βˆ…, π‘…βŸ©, ⟨1o, π‘†βŸ©}))
36 xpsvsca.k . . . 4 𝐾 = (Baseβ€˜πΊ)
37 eqid 2730 . . . 4 ( ·𝑠 β€˜(𝐺Xs{βŸ¨βˆ…, π‘…βŸ©, ⟨1o, π‘†βŸ©})) = ( ·𝑠 β€˜(𝐺Xs{βŸ¨βˆ…, π‘…βŸ©, ⟨1o, π‘†βŸ©}))
38 xpsvsca.p . . . 4 βˆ™ = ( ·𝑠 β€˜π‘‡)
3926f1ovscpbl 17476 . . . 4 ((πœ‘ ∧ (π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ ran (π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©}) ∧ 𝑐 ∈ ran (π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©}))) β†’ ((β—‘(π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©})β€˜π‘) = (β—‘(π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©})β€˜π‘) β†’ (β—‘(π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©})β€˜(π‘Ž( ·𝑠 β€˜(𝐺Xs{βŸ¨βˆ…, π‘…βŸ©, ⟨1o, π‘†βŸ©}))𝑏)) = (β—‘(π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©})β€˜(π‘Ž( ·𝑠 β€˜(𝐺Xs{βŸ¨βˆ…, π‘…βŸ©, ⟨1o, π‘†βŸ©}))𝑐))))
4023, 24, 28, 29, 35, 36, 37, 38, 39imasvscaval 17488 . . 3 ((πœ‘ ∧ 𝐴 ∈ 𝐾 ∧ {βŸ¨βˆ…, 𝐡⟩, ⟨1o, 𝐢⟩} ∈ ran (π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©})) β†’ (𝐴 βˆ™ (β—‘(π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©})β€˜{βŸ¨βˆ…, 𝐡⟩, ⟨1o, 𝐢⟩})) = (β—‘(π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©})β€˜(𝐴( ·𝑠 β€˜(𝐺Xs{βŸ¨βˆ…, π‘…βŸ©, ⟨1o, π‘†βŸ©})){βŸ¨βˆ…, 𝐡⟩, ⟨1o, 𝐢⟩})))
411, 15, 40mpd3an23 1461 . 2 (πœ‘ β†’ (𝐴 βˆ™ (β—‘(π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©})β€˜{βŸ¨βˆ…, 𝐡⟩, ⟨1o, 𝐢⟩})) = (β—‘(π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©})β€˜(𝐴( ·𝑠 β€˜(𝐺Xs{βŸ¨βˆ…, π‘…βŸ©, ⟨1o, π‘†βŸ©})){βŸ¨βˆ…, 𝐡⟩, ⟨1o, 𝐢⟩})))
42 f1ocnvfv 7278 . . . . 5 (((π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©}):(𝑋 Γ— π‘Œ)–1-1-ontoβ†’ran (π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©}) ∧ ⟨𝐡, 𝐢⟩ ∈ (𝑋 Γ— π‘Œ)) β†’ (((π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©})β€˜βŸ¨π΅, 𝐢⟩) = {βŸ¨βˆ…, 𝐡⟩, ⟨1o, 𝐢⟩} β†’ (β—‘(π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©})β€˜{βŸ¨βˆ…, 𝐡⟩, ⟨1o, 𝐢⟩}) = ⟨𝐡, 𝐢⟩))
4310, 9, 42sylancr 585 . . . 4 (πœ‘ β†’ (((π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©})β€˜βŸ¨π΅, 𝐢⟩) = {βŸ¨βˆ…, 𝐡⟩, ⟨1o, 𝐢⟩} β†’ (β—‘(π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©})β€˜{βŸ¨βˆ…, 𝐡⟩, ⟨1o, 𝐢⟩}) = ⟨𝐡, 𝐢⟩))
448, 43mpd 15 . . 3 (πœ‘ β†’ (β—‘(π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©})β€˜{βŸ¨βˆ…, 𝐡⟩, ⟨1o, 𝐢⟩}) = ⟨𝐡, 𝐢⟩)
4544oveq2d 7427 . 2 (πœ‘ β†’ (𝐴 βˆ™ (β—‘(π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©})β€˜{βŸ¨βˆ…, 𝐡⟩, ⟨1o, 𝐢⟩})) = (𝐴 βˆ™ ⟨𝐡, 𝐢⟩))
46 iftrue 4533 . . . . . . . . . . . 12 (π‘˜ = βˆ… β†’ if(π‘˜ = βˆ…, 𝑅, 𝑆) = 𝑅)
4746fveq2d 6894 . . . . . . . . . . 11 (π‘˜ = βˆ… β†’ ( ·𝑠 β€˜if(π‘˜ = βˆ…, 𝑅, 𝑆)) = ( ·𝑠 β€˜π‘…))
48 xpsvsca.m . . . . . . . . . . 11 Β· = ( ·𝑠 β€˜π‘…)
4947, 48eqtr4di 2788 . . . . . . . . . 10 (π‘˜ = βˆ… β†’ ( ·𝑠 β€˜if(π‘˜ = βˆ…, 𝑅, 𝑆)) = Β· )
50 eqidd 2731 . . . . . . . . . 10 (π‘˜ = βˆ… β†’ 𝐴 = 𝐴)
51 iftrue 4533 . . . . . . . . . 10 (π‘˜ = βˆ… β†’ if(π‘˜ = βˆ…, 𝐡, 𝐢) = 𝐡)
5249, 50, 51oveq123d 7432 . . . . . . . . 9 (π‘˜ = βˆ… β†’ (𝐴( ·𝑠 β€˜if(π‘˜ = βˆ…, 𝑅, 𝑆))if(π‘˜ = βˆ…, 𝐡, 𝐢)) = (𝐴 Β· 𝐡))
53 iftrue 4533 . . . . . . . . 9 (π‘˜ = βˆ… β†’ if(π‘˜ = βˆ…, (𝐴 Β· 𝐡), (𝐴 Γ— 𝐢)) = (𝐴 Β· 𝐡))
5452, 53eqtr4d 2773 . . . . . . . 8 (π‘˜ = βˆ… β†’ (𝐴( ·𝑠 β€˜if(π‘˜ = βˆ…, 𝑅, 𝑆))if(π‘˜ = βˆ…, 𝐡, 𝐢)) = if(π‘˜ = βˆ…, (𝐴 Β· 𝐡), (𝐴 Γ— 𝐢)))
55 iffalse 4536 . . . . . . . . . . . 12 (Β¬ π‘˜ = βˆ… β†’ if(π‘˜ = βˆ…, 𝑅, 𝑆) = 𝑆)
5655fveq2d 6894 . . . . . . . . . . 11 (Β¬ π‘˜ = βˆ… β†’ ( ·𝑠 β€˜if(π‘˜ = βˆ…, 𝑅, 𝑆)) = ( ·𝑠 β€˜π‘†))
57 xpsvsca.n . . . . . . . . . . 11 Γ— = ( ·𝑠 β€˜π‘†)
5856, 57eqtr4di 2788 . . . . . . . . . 10 (Β¬ π‘˜ = βˆ… β†’ ( ·𝑠 β€˜if(π‘˜ = βˆ…, 𝑅, 𝑆)) = Γ— )
59 eqidd 2731 . . . . . . . . . 10 (Β¬ π‘˜ = βˆ… β†’ 𝐴 = 𝐴)
60 iffalse 4536 . . . . . . . . . 10 (Β¬ π‘˜ = βˆ… β†’ if(π‘˜ = βˆ…, 𝐡, 𝐢) = 𝐢)
6158, 59, 60oveq123d 7432 . . . . . . . . 9 (Β¬ π‘˜ = βˆ… β†’ (𝐴( ·𝑠 β€˜if(π‘˜ = βˆ…, 𝑅, 𝑆))if(π‘˜ = βˆ…, 𝐡, 𝐢)) = (𝐴 Γ— 𝐢))
62 iffalse 4536 . . . . . . . . 9 (Β¬ π‘˜ = βˆ… β†’ if(π‘˜ = βˆ…, (𝐴 Β· 𝐡), (𝐴 Γ— 𝐢)) = (𝐴 Γ— 𝐢))
6361, 62eqtr4d 2773 . . . . . . . 8 (Β¬ π‘˜ = βˆ… β†’ (𝐴( ·𝑠 β€˜if(π‘˜ = βˆ…, 𝑅, 𝑆))if(π‘˜ = βˆ…, 𝐡, 𝐢)) = if(π‘˜ = βˆ…, (𝐴 Β· 𝐡), (𝐴 Γ— 𝐢)))
6454, 63pm2.61i 182 . . . . . . 7 (𝐴( ·𝑠 β€˜if(π‘˜ = βˆ…, 𝑅, 𝑆))if(π‘˜ = βˆ…, 𝐡, 𝐢)) = if(π‘˜ = βˆ…, (𝐴 Β· 𝐡), (𝐴 Γ— 𝐢))
6519adantr 479 . . . . . . . . . 10 ((πœ‘ ∧ π‘˜ ∈ 2o) β†’ 𝑅 ∈ 𝑉)
6620adantr 479 . . . . . . . . . 10 ((πœ‘ ∧ π‘˜ ∈ 2o) β†’ 𝑆 ∈ π‘Š)
67 simpr 483 . . . . . . . . . 10 ((πœ‘ ∧ π‘˜ ∈ 2o) β†’ π‘˜ ∈ 2o)
68 fvprif 17511 . . . . . . . . . 10 ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ π‘Š ∧ π‘˜ ∈ 2o) β†’ ({βŸ¨βˆ…, π‘…βŸ©, ⟨1o, π‘†βŸ©}β€˜π‘˜) = if(π‘˜ = βˆ…, 𝑅, 𝑆))
6965, 66, 67, 68syl3anc 1369 . . . . . . . . 9 ((πœ‘ ∧ π‘˜ ∈ 2o) β†’ ({βŸ¨βˆ…, π‘…βŸ©, ⟨1o, π‘†βŸ©}β€˜π‘˜) = if(π‘˜ = βˆ…, 𝑅, 𝑆))
7069fveq2d 6894 . . . . . . . 8 ((πœ‘ ∧ π‘˜ ∈ 2o) β†’ ( ·𝑠 β€˜({βŸ¨βˆ…, π‘…βŸ©, ⟨1o, π‘†βŸ©}β€˜π‘˜)) = ( ·𝑠 β€˜if(π‘˜ = βˆ…, 𝑅, 𝑆)))
71 eqidd 2731 . . . . . . . 8 ((πœ‘ ∧ π‘˜ ∈ 2o) β†’ 𝐴 = 𝐴)
723adantr 479 . . . . . . . . 9 ((πœ‘ ∧ π‘˜ ∈ 2o) β†’ 𝐡 ∈ 𝑋)
734adantr 479 . . . . . . . . 9 ((πœ‘ ∧ π‘˜ ∈ 2o) β†’ 𝐢 ∈ π‘Œ)
74 fvprif 17511 . . . . . . . . 9 ((𝐡 ∈ 𝑋 ∧ 𝐢 ∈ π‘Œ ∧ π‘˜ ∈ 2o) β†’ ({βŸ¨βˆ…, 𝐡⟩, ⟨1o, 𝐢⟩}β€˜π‘˜) = if(π‘˜ = βˆ…, 𝐡, 𝐢))
7572, 73, 67, 74syl3anc 1369 . . . . . . . 8 ((πœ‘ ∧ π‘˜ ∈ 2o) β†’ ({βŸ¨βˆ…, 𝐡⟩, ⟨1o, 𝐢⟩}β€˜π‘˜) = if(π‘˜ = βˆ…, 𝐡, 𝐢))
7670, 71, 75oveq123d 7432 . . . . . . 7 ((πœ‘ ∧ π‘˜ ∈ 2o) β†’ (𝐴( ·𝑠 β€˜({βŸ¨βˆ…, π‘…βŸ©, ⟨1o, π‘†βŸ©}β€˜π‘˜))({βŸ¨βˆ…, 𝐡⟩, ⟨1o, 𝐢⟩}β€˜π‘˜)) = (𝐴( ·𝑠 β€˜if(π‘˜ = βˆ…, 𝑅, 𝑆))if(π‘˜ = βˆ…, 𝐡, 𝐢)))
77 xpsvsca.6 . . . . . . . . 9 (πœ‘ β†’ (𝐴 Β· 𝐡) ∈ 𝑋)
7877adantr 479 . . . . . . . 8 ((πœ‘ ∧ π‘˜ ∈ 2o) β†’ (𝐴 Β· 𝐡) ∈ 𝑋)
79 xpsvsca.7 . . . . . . . . 9 (πœ‘ β†’ (𝐴 Γ— 𝐢) ∈ π‘Œ)
8079adantr 479 . . . . . . . 8 ((πœ‘ ∧ π‘˜ ∈ 2o) β†’ (𝐴 Γ— 𝐢) ∈ π‘Œ)
81 fvprif 17511 . . . . . . . 8 (((𝐴 Β· 𝐡) ∈ 𝑋 ∧ (𝐴 Γ— 𝐢) ∈ π‘Œ ∧ π‘˜ ∈ 2o) β†’ ({βŸ¨βˆ…, (𝐴 Β· 𝐡)⟩, ⟨1o, (𝐴 Γ— 𝐢)⟩}β€˜π‘˜) = if(π‘˜ = βˆ…, (𝐴 Β· 𝐡), (𝐴 Γ— 𝐢)))
8278, 80, 67, 81syl3anc 1369 . . . . . . 7 ((πœ‘ ∧ π‘˜ ∈ 2o) β†’ ({βŸ¨βˆ…, (𝐴 Β· 𝐡)⟩, ⟨1o, (𝐴 Γ— 𝐢)⟩}β€˜π‘˜) = if(π‘˜ = βˆ…, (𝐴 Β· 𝐡), (𝐴 Γ— 𝐢)))
8364, 76, 823eqtr4a 2796 . . . . . 6 ((πœ‘ ∧ π‘˜ ∈ 2o) β†’ (𝐴( ·𝑠 β€˜({βŸ¨βˆ…, π‘…βŸ©, ⟨1o, π‘†βŸ©}β€˜π‘˜))({βŸ¨βˆ…, 𝐡⟩, ⟨1o, 𝐢⟩}β€˜π‘˜)) = ({βŸ¨βˆ…, (𝐴 Β· 𝐡)⟩, ⟨1o, (𝐴 Γ— 𝐢)⟩}β€˜π‘˜))
8483mpteq2dva 5247 . . . . 5 (πœ‘ β†’ (π‘˜ ∈ 2o ↦ (𝐴( ·𝑠 β€˜({βŸ¨βˆ…, π‘…βŸ©, ⟨1o, π‘†βŸ©}β€˜π‘˜))({βŸ¨βˆ…, 𝐡⟩, ⟨1o, 𝐢⟩}β€˜π‘˜))) = (π‘˜ ∈ 2o ↦ ({βŸ¨βˆ…, (𝐴 Β· 𝐡)⟩, ⟨1o, (𝐴 Γ— 𝐢)⟩}β€˜π‘˜)))
85 eqid 2730 . . . . . 6 (Baseβ€˜(𝐺Xs{βŸ¨βˆ…, π‘…βŸ©, ⟨1o, π‘†βŸ©})) = (Baseβ€˜(𝐺Xs{βŸ¨βˆ…, π‘…βŸ©, ⟨1o, π‘†βŸ©}))
8630a1i 11 . . . . . 6 (πœ‘ β†’ 𝐺 ∈ V)
87 2on 8482 . . . . . . 7 2o ∈ On
8887a1i 11 . . . . . 6 (πœ‘ β†’ 2o ∈ On)
89 fnpr2o 17507 . . . . . . 7 ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ π‘Š) β†’ {βŸ¨βˆ…, π‘…βŸ©, ⟨1o, π‘†βŸ©} Fn 2o)
9019, 20, 89syl2anc 582 . . . . . 6 (πœ‘ β†’ {βŸ¨βˆ…, π‘…βŸ©, ⟨1o, π‘†βŸ©} Fn 2o)
9115, 24eleqtrd 2833 . . . . . 6 (πœ‘ β†’ {βŸ¨βˆ…, 𝐡⟩, ⟨1o, 𝐢⟩} ∈ (Baseβ€˜(𝐺Xs{βŸ¨βˆ…, π‘…βŸ©, ⟨1o, π‘†βŸ©})))
9222, 85, 37, 36, 86, 88, 90, 1, 91prdsvscaval 17429 . . . . 5 (πœ‘ β†’ (𝐴( ·𝑠 β€˜(𝐺Xs{βŸ¨βˆ…, π‘…βŸ©, ⟨1o, π‘†βŸ©})){βŸ¨βˆ…, 𝐡⟩, ⟨1o, 𝐢⟩}) = (π‘˜ ∈ 2o ↦ (𝐴( ·𝑠 β€˜({βŸ¨βˆ…, π‘…βŸ©, ⟨1o, π‘†βŸ©}β€˜π‘˜))({βŸ¨βˆ…, 𝐡⟩, ⟨1o, 𝐢⟩}β€˜π‘˜))))
93 fnpr2o 17507 . . . . . . 7 (((𝐴 Β· 𝐡) ∈ 𝑋 ∧ (𝐴 Γ— 𝐢) ∈ π‘Œ) β†’ {βŸ¨βˆ…, (𝐴 Β· 𝐡)⟩, ⟨1o, (𝐴 Γ— 𝐢)⟩} Fn 2o)
9477, 79, 93syl2anc 582 . . . . . 6 (πœ‘ β†’ {βŸ¨βˆ…, (𝐴 Β· 𝐡)⟩, ⟨1o, (𝐴 Γ— 𝐢)⟩} Fn 2o)
95 dffn5 6949 . . . . . 6 ({βŸ¨βˆ…, (𝐴 Β· 𝐡)⟩, ⟨1o, (𝐴 Γ— 𝐢)⟩} Fn 2o ↔ {βŸ¨βˆ…, (𝐴 Β· 𝐡)⟩, ⟨1o, (𝐴 Γ— 𝐢)⟩} = (π‘˜ ∈ 2o ↦ ({βŸ¨βˆ…, (𝐴 Β· 𝐡)⟩, ⟨1o, (𝐴 Γ— 𝐢)⟩}β€˜π‘˜)))
9694, 95sylib 217 . . . . 5 (πœ‘ β†’ {βŸ¨βˆ…, (𝐴 Β· 𝐡)⟩, ⟨1o, (𝐴 Γ— 𝐢)⟩} = (π‘˜ ∈ 2o ↦ ({βŸ¨βˆ…, (𝐴 Β· 𝐡)⟩, ⟨1o, (𝐴 Γ— 𝐢)⟩}β€˜π‘˜)))
9784, 92, 963eqtr4d 2780 . . . 4 (πœ‘ β†’ (𝐴( ·𝑠 β€˜(𝐺Xs{βŸ¨βˆ…, π‘…βŸ©, ⟨1o, π‘†βŸ©})){βŸ¨βˆ…, 𝐡⟩, ⟨1o, 𝐢⟩}) = {βŸ¨βˆ…, (𝐴 Β· 𝐡)⟩, ⟨1o, (𝐴 Γ— 𝐢)⟩})
9897fveq2d 6894 . . 3 (πœ‘ β†’ (β—‘(π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©})β€˜(𝐴( ·𝑠 β€˜(𝐺Xs{βŸ¨βˆ…, π‘…βŸ©, ⟨1o, π‘†βŸ©})){βŸ¨βˆ…, 𝐡⟩, ⟨1o, 𝐢⟩})) = (β—‘(π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©})β€˜{βŸ¨βˆ…, (𝐴 Β· 𝐡)⟩, ⟨1o, (𝐴 Γ— 𝐢)⟩}))
99 df-ov 7414 . . . . 5 ((𝐴 Β· 𝐡)(π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©})(𝐴 Γ— 𝐢)) = ((π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©})β€˜βŸ¨(𝐴 Β· 𝐡), (𝐴 Γ— 𝐢)⟩)
1005xpsfval 17516 . . . . . 6 (((𝐴 Β· 𝐡) ∈ 𝑋 ∧ (𝐴 Γ— 𝐢) ∈ π‘Œ) β†’ ((𝐴 Β· 𝐡)(π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©})(𝐴 Γ— 𝐢)) = {βŸ¨βˆ…, (𝐴 Β· 𝐡)⟩, ⟨1o, (𝐴 Γ— 𝐢)⟩})
10177, 79, 100syl2anc 582 . . . . 5 (πœ‘ β†’ ((𝐴 Β· 𝐡)(π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©})(𝐴 Γ— 𝐢)) = {βŸ¨βˆ…, (𝐴 Β· 𝐡)⟩, ⟨1o, (𝐴 Γ— 𝐢)⟩})
10299, 101eqtr3id 2784 . . . 4 (πœ‘ β†’ ((π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©})β€˜βŸ¨(𝐴 Β· 𝐡), (𝐴 Γ— 𝐢)⟩) = {βŸ¨βˆ…, (𝐴 Β· 𝐡)⟩, ⟨1o, (𝐴 Γ— 𝐢)⟩})
10377, 79opelxpd 5714 . . . . 5 (πœ‘ β†’ ⟨(𝐴 Β· 𝐡), (𝐴 Γ— 𝐢)⟩ ∈ (𝑋 Γ— π‘Œ))
104 f1ocnvfv 7278 . . . . 5 (((π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©}):(𝑋 Γ— π‘Œ)–1-1-ontoβ†’ran (π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©}) ∧ ⟨(𝐴 Β· 𝐡), (𝐴 Γ— 𝐢)⟩ ∈ (𝑋 Γ— π‘Œ)) β†’ (((π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©})β€˜βŸ¨(𝐴 Β· 𝐡), (𝐴 Γ— 𝐢)⟩) = {βŸ¨βˆ…, (𝐴 Β· 𝐡)⟩, ⟨1o, (𝐴 Γ— 𝐢)⟩} β†’ (β—‘(π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©})β€˜{βŸ¨βˆ…, (𝐴 Β· 𝐡)⟩, ⟨1o, (𝐴 Γ— 𝐢)⟩}) = ⟨(𝐴 Β· 𝐡), (𝐴 Γ— 𝐢)⟩))
10510, 103, 104sylancr 585 . . . 4 (πœ‘ β†’ (((π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©})β€˜βŸ¨(𝐴 Β· 𝐡), (𝐴 Γ— 𝐢)⟩) = {βŸ¨βˆ…, (𝐴 Β· 𝐡)⟩, ⟨1o, (𝐴 Γ— 𝐢)⟩} β†’ (β—‘(π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©})β€˜{βŸ¨βˆ…, (𝐴 Β· 𝐡)⟩, ⟨1o, (𝐴 Γ— 𝐢)⟩}) = ⟨(𝐴 Β· 𝐡), (𝐴 Γ— 𝐢)⟩))
106102, 105mpd 15 . . 3 (πœ‘ β†’ (β—‘(π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©})β€˜{βŸ¨βˆ…, (𝐴 Β· 𝐡)⟩, ⟨1o, (𝐴 Γ— 𝐢)⟩}) = ⟨(𝐴 Β· 𝐡), (𝐴 Γ— 𝐢)⟩)
10798, 106eqtrd 2770 . 2 (πœ‘ β†’ (β—‘(π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©})β€˜(𝐴( ·𝑠 β€˜(𝐺Xs{βŸ¨βˆ…, π‘…βŸ©, ⟨1o, π‘†βŸ©})){βŸ¨βˆ…, 𝐡⟩, ⟨1o, 𝐢⟩})) = ⟨(𝐴 Β· 𝐡), (𝐴 Γ— 𝐢)⟩)
10841, 45, 1073eqtr3d 2778 1 (πœ‘ β†’ (𝐴 βˆ™ ⟨𝐡, 𝐢⟩) = ⟨(𝐴 Β· 𝐡), (𝐴 Γ— 𝐢)⟩)
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ∧ wa 394   = wceq 1539  βŠ€wtru 1540   ∈ wcel 2104  Vcvv 3472  βˆ…c0 4321  ifcif 4527  {cpr 4629  βŸ¨cop 4633   ↦ cmpt 5230   Γ— cxp 5673  β—‘ccnv 5674  ran crn 5676  Oncon0 6363   Fn wfn 6537  βŸΆwf 6538  β€“ontoβ†’wfo 6540  β€“1-1-ontoβ†’wf1o 6541  β€˜cfv 6542  (class class class)co 7411   ∈ cmpo 7413  1oc1o 8461  2oc2o 8462  Basecbs 17148  Scalarcsca 17204   ·𝑠 cvsca 17205  Xscprds 17395   Γ—s cxps 17456
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7727  ax-cnex 11168  ax-resscn 11169  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-addrcl 11173  ax-mulcl 11174  ax-mulrcl 11175  ax-mulcom 11176  ax-addass 11177  ax-mulass 11178  ax-distr 11179  ax-i2m1 11180  ax-1ne0 11181  ax-1rid 11182  ax-rnegex 11183  ax-rrecex 11184  ax-cnre 11185  ax-pre-lttri 11186  ax-pre-lttrn 11187  ax-pre-ltadd 11188  ax-pre-mulgt0 11189
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-reu 3375  df-rab 3431  df-v 3474  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-tp 4632  df-op 4634  df-uni 4908  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6299  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-riota 7367  df-ov 7414  df-oprab 7415  df-mpo 7416  df-om 7858  df-1st 7977  df-2nd 7978  df-frecs 8268  df-wrecs 8299  df-recs 8373  df-rdg 8412  df-1o 8468  df-2o 8469  df-er 8705  df-map 8824  df-ixp 8894  df-en 8942  df-dom 8943  df-sdom 8944  df-fin 8945  df-sup 9439  df-inf 9440  df-pnf 11254  df-mnf 11255  df-xr 11256  df-ltxr 11257  df-le 11258  df-sub 11450  df-neg 11451  df-nn 12217  df-2 12279  df-3 12280  df-4 12281  df-5 12282  df-6 12283  df-7 12284  df-8 12285  df-9 12286  df-n0 12477  df-z 12563  df-dec 12682  df-uz 12827  df-fz 13489  df-struct 17084  df-slot 17119  df-ndx 17131  df-base 17149  df-plusg 17214  df-mulr 17215  df-sca 17217  df-vsca 17218  df-ip 17219  df-tset 17220  df-ple 17221  df-ds 17223  df-hom 17225  df-cco 17226  df-prds 17397  df-imas 17458  df-xps 17460
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator