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

Theorem xpsvsca 17460
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 7361 . . . . 5 (𝐡(π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©})𝐢) = ((π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©})β€˜βŸ¨π΅, 𝐢⟩)
3 xpsvsca.4 . . . . . 6 (πœ‘ β†’ 𝐡 ∈ 𝑋)
4 xpsvsca.5 . . . . . 6 (πœ‘ β†’ 𝐢 ∈ π‘Œ)
5 eqid 2737 . . . . . . 7 (π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©}) = (π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©})
65xpsfval 17449 . . . . . 6 ((𝐡 ∈ 𝑋 ∧ 𝐢 ∈ π‘Œ) β†’ (𝐡(π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©})𝐢) = {βŸ¨βˆ…, 𝐡⟩, ⟨1o, 𝐢⟩})
73, 4, 6syl2anc 585 . . . . 5 (πœ‘ β†’ (𝐡(π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©})𝐢) = {βŸ¨βˆ…, 𝐡⟩, ⟨1o, 𝐢⟩})
82, 7eqtr3id 2791 . . . 4 (πœ‘ β†’ ((π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©})β€˜βŸ¨π΅, 𝐢⟩) = {βŸ¨βˆ…, 𝐡⟩, ⟨1o, 𝐢⟩})
93, 4opelxpd 5672 . . . . 5 (πœ‘ β†’ ⟨𝐡, 𝐢⟩ ∈ (𝑋 Γ— π‘Œ))
105xpsff1o2 17452 . . . . . . 7 (π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©}):(𝑋 Γ— π‘Œ)–1-1-ontoβ†’ran (π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©})
11 f1of 6785 . . . . . . 7 ((π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©}):(𝑋 Γ— π‘Œ)–1-1-ontoβ†’ran (π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©}) β†’ (π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©}):(𝑋 Γ— π‘Œ)⟢ran (π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©}))
1210, 11ax-mp 5 . . . . . 6 (π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©}):(𝑋 Γ— π‘Œ)⟢ran (π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©})
1312ffvelcdmi 7035 . . . . 5 (⟨𝐡, 𝐢⟩ ∈ (𝑋 Γ— π‘Œ) β†’ ((π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©})β€˜βŸ¨π΅, 𝐢⟩) ∈ ran (π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©}))
149, 13syl 17 . . . 4 (πœ‘ β†’ ((π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©})β€˜βŸ¨π΅, 𝐢⟩) ∈ ran (π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©}))
158, 14eqeltrrd 2839 . . 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 2737 . . . . 5 (𝐺Xs{βŸ¨βˆ…, π‘…βŸ©, ⟨1o, π‘†βŸ©}) = (𝐺Xs{βŸ¨βˆ…, π‘…βŸ©, ⟨1o, π‘†βŸ©})
2316, 17, 18, 19, 20, 5, 21, 22xpsval 17453 . . . 4 (πœ‘ β†’ 𝑇 = (β—‘(π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©}) β€œs (𝐺Xs{βŸ¨βˆ…, π‘…βŸ©, ⟨1o, π‘†βŸ©})))
2416, 17, 18, 19, 20, 5, 21, 22xpsrnbas 17454 . . . 4 (πœ‘ β†’ ran (π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©}) = (Baseβ€˜(𝐺Xs{βŸ¨βˆ…, π‘…βŸ©, ⟨1o, π‘†βŸ©})))
25 f1ocnv 6797 . . . . . 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 6792 . . . . 5 (β—‘(π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©}):ran (π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©})–1-1-ontoβ†’(𝑋 Γ— π‘Œ) β†’ β—‘(π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©}):ran (π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©})–ontoβ†’(𝑋 Γ— π‘Œ))
2826, 27syl 17 . . . 4 (πœ‘ β†’ β—‘(π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©}):ran (π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©})–ontoβ†’(𝑋 Γ— π‘Œ))
29 ovexd 7393 . . . 4 (πœ‘ β†’ (𝐺Xs{βŸ¨βˆ…, π‘…βŸ©, ⟨1o, π‘†βŸ©}) ∈ V)
3021fvexi 6857 . . . . . . 7 𝐺 ∈ V
3130a1i 11 . . . . . 6 (⊀ β†’ 𝐺 ∈ V)
32 prex 5390 . . . . . . 7 {βŸ¨βˆ…, π‘…βŸ©, ⟨1o, π‘†βŸ©} ∈ V
3332a1i 11 . . . . . 6 (⊀ β†’ {βŸ¨βˆ…, π‘…βŸ©, ⟨1o, π‘†βŸ©} ∈ V)
3422, 31, 33prdssca 17339 . . . . 5 (⊀ β†’ 𝐺 = (Scalarβ€˜(𝐺Xs{βŸ¨βˆ…, π‘…βŸ©, ⟨1o, π‘†βŸ©})))
3534mptru 1549 . . . 4 𝐺 = (Scalarβ€˜(𝐺Xs{βŸ¨βˆ…, π‘…βŸ©, ⟨1o, π‘†βŸ©}))
36 xpsvsca.k . . . 4 𝐾 = (Baseβ€˜πΊ)
37 eqid 2737 . . . 4 ( ·𝑠 β€˜(𝐺Xs{βŸ¨βˆ…, π‘…βŸ©, ⟨1o, π‘†βŸ©})) = ( ·𝑠 β€˜(𝐺Xs{βŸ¨βˆ…, π‘…βŸ©, ⟨1o, π‘†βŸ©}))
38 xpsvsca.p . . . 4 βˆ™ = ( ·𝑠 β€˜π‘‡)
3926f1ovscpbl 17409 . . . 4 ((πœ‘ ∧ (π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ ran (π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©}) ∧ 𝑐 ∈ ran (π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©}))) β†’ ((β—‘(π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©})β€˜π‘) = (β—‘(π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©})β€˜π‘) β†’ (β—‘(π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©})β€˜(π‘Ž( ·𝑠 β€˜(𝐺Xs{βŸ¨βˆ…, π‘…βŸ©, ⟨1o, π‘†βŸ©}))𝑏)) = (β—‘(π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©})β€˜(π‘Ž( ·𝑠 β€˜(𝐺Xs{βŸ¨βˆ…, π‘…βŸ©, ⟨1o, π‘†βŸ©}))𝑐))))
4023, 24, 28, 29, 35, 36, 37, 38, 39imasvscaval 17421 . . 3 ((πœ‘ ∧ 𝐴 ∈ 𝐾 ∧ {βŸ¨βˆ…, 𝐡⟩, ⟨1o, 𝐢⟩} ∈ ran (π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©})) β†’ (𝐴 βˆ™ (β—‘(π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©})β€˜{βŸ¨βˆ…, 𝐡⟩, ⟨1o, 𝐢⟩})) = (β—‘(π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©})β€˜(𝐴( ·𝑠 β€˜(𝐺Xs{βŸ¨βˆ…, π‘…βŸ©, ⟨1o, π‘†βŸ©})){βŸ¨βˆ…, 𝐡⟩, ⟨1o, 𝐢⟩})))
411, 15, 40mpd3an23 1464 . 2 (πœ‘ β†’ (𝐴 βˆ™ (β—‘(π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©})β€˜{βŸ¨βˆ…, 𝐡⟩, ⟨1o, 𝐢⟩})) = (β—‘(π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©})β€˜(𝐴( ·𝑠 β€˜(𝐺Xs{βŸ¨βˆ…, π‘…βŸ©, ⟨1o, π‘†βŸ©})){βŸ¨βˆ…, 𝐡⟩, ⟨1o, 𝐢⟩})))
42 f1ocnvfv 7225 . . . . 5 (((π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©}):(𝑋 Γ— π‘Œ)–1-1-ontoβ†’ran (π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©}) ∧ ⟨𝐡, 𝐢⟩ ∈ (𝑋 Γ— π‘Œ)) β†’ (((π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©})β€˜βŸ¨π΅, 𝐢⟩) = {βŸ¨βˆ…, 𝐡⟩, ⟨1o, 𝐢⟩} β†’ (β—‘(π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©})β€˜{βŸ¨βˆ…, 𝐡⟩, ⟨1o, 𝐢⟩}) = ⟨𝐡, 𝐢⟩))
4310, 9, 42sylancr 588 . . . 4 (πœ‘ β†’ (((π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©})β€˜βŸ¨π΅, 𝐢⟩) = {βŸ¨βˆ…, 𝐡⟩, ⟨1o, 𝐢⟩} β†’ (β—‘(π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©})β€˜{βŸ¨βˆ…, 𝐡⟩, ⟨1o, 𝐢⟩}) = ⟨𝐡, 𝐢⟩))
448, 43mpd 15 . . 3 (πœ‘ β†’ (β—‘(π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©})β€˜{βŸ¨βˆ…, 𝐡⟩, ⟨1o, 𝐢⟩}) = ⟨𝐡, 𝐢⟩)
4544oveq2d 7374 . 2 (πœ‘ β†’ (𝐴 βˆ™ (β—‘(π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©})β€˜{βŸ¨βˆ…, 𝐡⟩, ⟨1o, 𝐢⟩})) = (𝐴 βˆ™ ⟨𝐡, 𝐢⟩))
46 iftrue 4493 . . . . . . . . . . . 12 (π‘˜ = βˆ… β†’ if(π‘˜ = βˆ…, 𝑅, 𝑆) = 𝑅)
4746fveq2d 6847 . . . . . . . . . . 11 (π‘˜ = βˆ… β†’ ( ·𝑠 β€˜if(π‘˜ = βˆ…, 𝑅, 𝑆)) = ( ·𝑠 β€˜π‘…))
48 xpsvsca.m . . . . . . . . . . 11 Β· = ( ·𝑠 β€˜π‘…)
4947, 48eqtr4di 2795 . . . . . . . . . 10 (π‘˜ = βˆ… β†’ ( ·𝑠 β€˜if(π‘˜ = βˆ…, 𝑅, 𝑆)) = Β· )
50 eqidd 2738 . . . . . . . . . 10 (π‘˜ = βˆ… β†’ 𝐴 = 𝐴)
51 iftrue 4493 . . . . . . . . . 10 (π‘˜ = βˆ… β†’ if(π‘˜ = βˆ…, 𝐡, 𝐢) = 𝐡)
5249, 50, 51oveq123d 7379 . . . . . . . . 9 (π‘˜ = βˆ… β†’ (𝐴( ·𝑠 β€˜if(π‘˜ = βˆ…, 𝑅, 𝑆))if(π‘˜ = βˆ…, 𝐡, 𝐢)) = (𝐴 Β· 𝐡))
53 iftrue 4493 . . . . . . . . 9 (π‘˜ = βˆ… β†’ if(π‘˜ = βˆ…, (𝐴 Β· 𝐡), (𝐴 Γ— 𝐢)) = (𝐴 Β· 𝐡))
5452, 53eqtr4d 2780 . . . . . . . 8 (π‘˜ = βˆ… β†’ (𝐴( ·𝑠 β€˜if(π‘˜ = βˆ…, 𝑅, 𝑆))if(π‘˜ = βˆ…, 𝐡, 𝐢)) = if(π‘˜ = βˆ…, (𝐴 Β· 𝐡), (𝐴 Γ— 𝐢)))
55 iffalse 4496 . . . . . . . . . . . 12 (Β¬ π‘˜ = βˆ… β†’ if(π‘˜ = βˆ…, 𝑅, 𝑆) = 𝑆)
5655fveq2d 6847 . . . . . . . . . . 11 (Β¬ π‘˜ = βˆ… β†’ ( ·𝑠 β€˜if(π‘˜ = βˆ…, 𝑅, 𝑆)) = ( ·𝑠 β€˜π‘†))
57 xpsvsca.n . . . . . . . . . . 11 Γ— = ( ·𝑠 β€˜π‘†)
5856, 57eqtr4di 2795 . . . . . . . . . 10 (Β¬ π‘˜ = βˆ… β†’ ( ·𝑠 β€˜if(π‘˜ = βˆ…, 𝑅, 𝑆)) = Γ— )
59 eqidd 2738 . . . . . . . . . 10 (Β¬ π‘˜ = βˆ… β†’ 𝐴 = 𝐴)
60 iffalse 4496 . . . . . . . . . 10 (Β¬ π‘˜ = βˆ… β†’ if(π‘˜ = βˆ…, 𝐡, 𝐢) = 𝐢)
6158, 59, 60oveq123d 7379 . . . . . . . . 9 (Β¬ π‘˜ = βˆ… β†’ (𝐴( ·𝑠 β€˜if(π‘˜ = βˆ…, 𝑅, 𝑆))if(π‘˜ = βˆ…, 𝐡, 𝐢)) = (𝐴 Γ— 𝐢))
62 iffalse 4496 . . . . . . . . 9 (Β¬ π‘˜ = βˆ… β†’ if(π‘˜ = βˆ…, (𝐴 Β· 𝐡), (𝐴 Γ— 𝐢)) = (𝐴 Γ— 𝐢))
6361, 62eqtr4d 2780 . . . . . . . 8 (Β¬ π‘˜ = βˆ… β†’ (𝐴( ·𝑠 β€˜if(π‘˜ = βˆ…, 𝑅, 𝑆))if(π‘˜ = βˆ…, 𝐡, 𝐢)) = if(π‘˜ = βˆ…, (𝐴 Β· 𝐡), (𝐴 Γ— 𝐢)))
6454, 63pm2.61i 182 . . . . . . 7 (𝐴( ·𝑠 β€˜if(π‘˜ = βˆ…, 𝑅, 𝑆))if(π‘˜ = βˆ…, 𝐡, 𝐢)) = if(π‘˜ = βˆ…, (𝐴 Β· 𝐡), (𝐴 Γ— 𝐢))
6519adantr 482 . . . . . . . . . 10 ((πœ‘ ∧ π‘˜ ∈ 2o) β†’ 𝑅 ∈ 𝑉)
6620adantr 482 . . . . . . . . . 10 ((πœ‘ ∧ π‘˜ ∈ 2o) β†’ 𝑆 ∈ π‘Š)
67 simpr 486 . . . . . . . . . 10 ((πœ‘ ∧ π‘˜ ∈ 2o) β†’ π‘˜ ∈ 2o)
68 fvprif 17444 . . . . . . . . . 10 ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ π‘Š ∧ π‘˜ ∈ 2o) β†’ ({βŸ¨βˆ…, π‘…βŸ©, ⟨1o, π‘†βŸ©}β€˜π‘˜) = if(π‘˜ = βˆ…, 𝑅, 𝑆))
6965, 66, 67, 68syl3anc 1372 . . . . . . . . 9 ((πœ‘ ∧ π‘˜ ∈ 2o) β†’ ({βŸ¨βˆ…, π‘…βŸ©, ⟨1o, π‘†βŸ©}β€˜π‘˜) = if(π‘˜ = βˆ…, 𝑅, 𝑆))
7069fveq2d 6847 . . . . . . . 8 ((πœ‘ ∧ π‘˜ ∈ 2o) β†’ ( ·𝑠 β€˜({βŸ¨βˆ…, π‘…βŸ©, ⟨1o, π‘†βŸ©}β€˜π‘˜)) = ( ·𝑠 β€˜if(π‘˜ = βˆ…, 𝑅, 𝑆)))
71 eqidd 2738 . . . . . . . 8 ((πœ‘ ∧ π‘˜ ∈ 2o) β†’ 𝐴 = 𝐴)
723adantr 482 . . . . . . . . 9 ((πœ‘ ∧ π‘˜ ∈ 2o) β†’ 𝐡 ∈ 𝑋)
734adantr 482 . . . . . . . . 9 ((πœ‘ ∧ π‘˜ ∈ 2o) β†’ 𝐢 ∈ π‘Œ)
74 fvprif 17444 . . . . . . . . 9 ((𝐡 ∈ 𝑋 ∧ 𝐢 ∈ π‘Œ ∧ π‘˜ ∈ 2o) β†’ ({βŸ¨βˆ…, 𝐡⟩, ⟨1o, 𝐢⟩}β€˜π‘˜) = if(π‘˜ = βˆ…, 𝐡, 𝐢))
7572, 73, 67, 74syl3anc 1372 . . . . . . . 8 ((πœ‘ ∧ π‘˜ ∈ 2o) β†’ ({βŸ¨βˆ…, 𝐡⟩, ⟨1o, 𝐢⟩}β€˜π‘˜) = if(π‘˜ = βˆ…, 𝐡, 𝐢))
7670, 71, 75oveq123d 7379 . . . . . . 7 ((πœ‘ ∧ π‘˜ ∈ 2o) β†’ (𝐴( ·𝑠 β€˜({βŸ¨βˆ…, π‘…βŸ©, ⟨1o, π‘†βŸ©}β€˜π‘˜))({βŸ¨βˆ…, 𝐡⟩, ⟨1o, 𝐢⟩}β€˜π‘˜)) = (𝐴( ·𝑠 β€˜if(π‘˜ = βˆ…, 𝑅, 𝑆))if(π‘˜ = βˆ…, 𝐡, 𝐢)))
77 xpsvsca.6 . . . . . . . . 9 (πœ‘ β†’ (𝐴 Β· 𝐡) ∈ 𝑋)
7877adantr 482 . . . . . . . 8 ((πœ‘ ∧ π‘˜ ∈ 2o) β†’ (𝐴 Β· 𝐡) ∈ 𝑋)
79 xpsvsca.7 . . . . . . . . 9 (πœ‘ β†’ (𝐴 Γ— 𝐢) ∈ π‘Œ)
8079adantr 482 . . . . . . . 8 ((πœ‘ ∧ π‘˜ ∈ 2o) β†’ (𝐴 Γ— 𝐢) ∈ π‘Œ)
81 fvprif 17444 . . . . . . . 8 (((𝐴 Β· 𝐡) ∈ 𝑋 ∧ (𝐴 Γ— 𝐢) ∈ π‘Œ ∧ π‘˜ ∈ 2o) β†’ ({βŸ¨βˆ…, (𝐴 Β· 𝐡)⟩, ⟨1o, (𝐴 Γ— 𝐢)⟩}β€˜π‘˜) = if(π‘˜ = βˆ…, (𝐴 Β· 𝐡), (𝐴 Γ— 𝐢)))
8278, 80, 67, 81syl3anc 1372 . . . . . . 7 ((πœ‘ ∧ π‘˜ ∈ 2o) β†’ ({βŸ¨βˆ…, (𝐴 Β· 𝐡)⟩, ⟨1o, (𝐴 Γ— 𝐢)⟩}β€˜π‘˜) = if(π‘˜ = βˆ…, (𝐴 Β· 𝐡), (𝐴 Γ— 𝐢)))
8364, 76, 823eqtr4a 2803 . . . . . 6 ((πœ‘ ∧ π‘˜ ∈ 2o) β†’ (𝐴( ·𝑠 β€˜({βŸ¨βˆ…, π‘…βŸ©, ⟨1o, π‘†βŸ©}β€˜π‘˜))({βŸ¨βˆ…, 𝐡⟩, ⟨1o, 𝐢⟩}β€˜π‘˜)) = ({βŸ¨βˆ…, (𝐴 Β· 𝐡)⟩, ⟨1o, (𝐴 Γ— 𝐢)⟩}β€˜π‘˜))
8483mpteq2dva 5206 . . . . 5 (πœ‘ β†’ (π‘˜ ∈ 2o ↦ (𝐴( ·𝑠 β€˜({βŸ¨βˆ…, π‘…βŸ©, ⟨1o, π‘†βŸ©}β€˜π‘˜))({βŸ¨βˆ…, 𝐡⟩, ⟨1o, 𝐢⟩}β€˜π‘˜))) = (π‘˜ ∈ 2o ↦ ({βŸ¨βˆ…, (𝐴 Β· 𝐡)⟩, ⟨1o, (𝐴 Γ— 𝐢)⟩}β€˜π‘˜)))
85 eqid 2737 . . . . . 6 (Baseβ€˜(𝐺Xs{βŸ¨βˆ…, π‘…βŸ©, ⟨1o, π‘†βŸ©})) = (Baseβ€˜(𝐺Xs{βŸ¨βˆ…, π‘…βŸ©, ⟨1o, π‘†βŸ©}))
8630a1i 11 . . . . . 6 (πœ‘ β†’ 𝐺 ∈ V)
87 2on 8427 . . . . . . 7 2o ∈ On
8887a1i 11 . . . . . 6 (πœ‘ β†’ 2o ∈ On)
89 fnpr2o 17440 . . . . . . 7 ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ π‘Š) β†’ {βŸ¨βˆ…, π‘…βŸ©, ⟨1o, π‘†βŸ©} Fn 2o)
9019, 20, 89syl2anc 585 . . . . . 6 (πœ‘ β†’ {βŸ¨βˆ…, π‘…βŸ©, ⟨1o, π‘†βŸ©} Fn 2o)
9115, 24eleqtrd 2840 . . . . . 6 (πœ‘ β†’ {βŸ¨βˆ…, 𝐡⟩, ⟨1o, 𝐢⟩} ∈ (Baseβ€˜(𝐺Xs{βŸ¨βˆ…, π‘…βŸ©, ⟨1o, π‘†βŸ©})))
9222, 85, 37, 36, 86, 88, 90, 1, 91prdsvscaval 17362 . . . . 5 (πœ‘ β†’ (𝐴( ·𝑠 β€˜(𝐺Xs{βŸ¨βˆ…, π‘…βŸ©, ⟨1o, π‘†βŸ©})){βŸ¨βˆ…, 𝐡⟩, ⟨1o, 𝐢⟩}) = (π‘˜ ∈ 2o ↦ (𝐴( ·𝑠 β€˜({βŸ¨βˆ…, π‘…βŸ©, ⟨1o, π‘†βŸ©}β€˜π‘˜))({βŸ¨βˆ…, 𝐡⟩, ⟨1o, 𝐢⟩}β€˜π‘˜))))
93 fnpr2o 17440 . . . . . . 7 (((𝐴 Β· 𝐡) ∈ 𝑋 ∧ (𝐴 Γ— 𝐢) ∈ π‘Œ) β†’ {βŸ¨βˆ…, (𝐴 Β· 𝐡)⟩, ⟨1o, (𝐴 Γ— 𝐢)⟩} Fn 2o)
9477, 79, 93syl2anc 585 . . . . . 6 (πœ‘ β†’ {βŸ¨βˆ…, (𝐴 Β· 𝐡)⟩, ⟨1o, (𝐴 Γ— 𝐢)⟩} Fn 2o)
95 dffn5 6902 . . . . . 6 ({βŸ¨βˆ…, (𝐴 Β· 𝐡)⟩, ⟨1o, (𝐴 Γ— 𝐢)⟩} Fn 2o ↔ {βŸ¨βˆ…, (𝐴 Β· 𝐡)⟩, ⟨1o, (𝐴 Γ— 𝐢)⟩} = (π‘˜ ∈ 2o ↦ ({βŸ¨βˆ…, (𝐴 Β· 𝐡)⟩, ⟨1o, (𝐴 Γ— 𝐢)⟩}β€˜π‘˜)))
9694, 95sylib 217 . . . . 5 (πœ‘ β†’ {βŸ¨βˆ…, (𝐴 Β· 𝐡)⟩, ⟨1o, (𝐴 Γ— 𝐢)⟩} = (π‘˜ ∈ 2o ↦ ({βŸ¨βˆ…, (𝐴 Β· 𝐡)⟩, ⟨1o, (𝐴 Γ— 𝐢)⟩}β€˜π‘˜)))
9784, 92, 963eqtr4d 2787 . . . 4 (πœ‘ β†’ (𝐴( ·𝑠 β€˜(𝐺Xs{βŸ¨βˆ…, π‘…βŸ©, ⟨1o, π‘†βŸ©})){βŸ¨βˆ…, 𝐡⟩, ⟨1o, 𝐢⟩}) = {βŸ¨βˆ…, (𝐴 Β· 𝐡)⟩, ⟨1o, (𝐴 Γ— 𝐢)⟩})
9897fveq2d 6847 . . 3 (πœ‘ β†’ (β—‘(π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©})β€˜(𝐴( ·𝑠 β€˜(𝐺Xs{βŸ¨βˆ…, π‘…βŸ©, ⟨1o, π‘†βŸ©})){βŸ¨βˆ…, 𝐡⟩, ⟨1o, 𝐢⟩})) = (β—‘(π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©})β€˜{βŸ¨βˆ…, (𝐴 Β· 𝐡)⟩, ⟨1o, (𝐴 Γ— 𝐢)⟩}))
99 df-ov 7361 . . . . 5 ((𝐴 Β· 𝐡)(π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©})(𝐴 Γ— 𝐢)) = ((π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©})β€˜βŸ¨(𝐴 Β· 𝐡), (𝐴 Γ— 𝐢)⟩)
1005xpsfval 17449 . . . . . 6 (((𝐴 Β· 𝐡) ∈ 𝑋 ∧ (𝐴 Γ— 𝐢) ∈ π‘Œ) β†’ ((𝐴 Β· 𝐡)(π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©})(𝐴 Γ— 𝐢)) = {βŸ¨βˆ…, (𝐴 Β· 𝐡)⟩, ⟨1o, (𝐴 Γ— 𝐢)⟩})
10177, 79, 100syl2anc 585 . . . . 5 (πœ‘ β†’ ((𝐴 Β· 𝐡)(π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©})(𝐴 Γ— 𝐢)) = {βŸ¨βˆ…, (𝐴 Β· 𝐡)⟩, ⟨1o, (𝐴 Γ— 𝐢)⟩})
10299, 101eqtr3id 2791 . . . 4 (πœ‘ β†’ ((π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©})β€˜βŸ¨(𝐴 Β· 𝐡), (𝐴 Γ— 𝐢)⟩) = {βŸ¨βˆ…, (𝐴 Β· 𝐡)⟩, ⟨1o, (𝐴 Γ— 𝐢)⟩})
10377, 79opelxpd 5672 . . . . 5 (πœ‘ β†’ ⟨(𝐴 Β· 𝐡), (𝐴 Γ— 𝐢)⟩ ∈ (𝑋 Γ— π‘Œ))
104 f1ocnvfv 7225 . . . . 5 (((π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©}):(𝑋 Γ— π‘Œ)–1-1-ontoβ†’ran (π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©}) ∧ ⟨(𝐴 Β· 𝐡), (𝐴 Γ— 𝐢)⟩ ∈ (𝑋 Γ— π‘Œ)) β†’ (((π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©})β€˜βŸ¨(𝐴 Β· 𝐡), (𝐴 Γ— 𝐢)⟩) = {βŸ¨βˆ…, (𝐴 Β· 𝐡)⟩, ⟨1o, (𝐴 Γ— 𝐢)⟩} β†’ (β—‘(π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©})β€˜{βŸ¨βˆ…, (𝐴 Β· 𝐡)⟩, ⟨1o, (𝐴 Γ— 𝐢)⟩}) = ⟨(𝐴 Β· 𝐡), (𝐴 Γ— 𝐢)⟩))
10510, 103, 104sylancr 588 . . . 4 (πœ‘ β†’ (((π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©})β€˜βŸ¨(𝐴 Β· 𝐡), (𝐴 Γ— 𝐢)⟩) = {βŸ¨βˆ…, (𝐴 Β· 𝐡)⟩, ⟨1o, (𝐴 Γ— 𝐢)⟩} β†’ (β—‘(π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©})β€˜{βŸ¨βˆ…, (𝐴 Β· 𝐡)⟩, ⟨1o, (𝐴 Γ— 𝐢)⟩}) = ⟨(𝐴 Β· 𝐡), (𝐴 Γ— 𝐢)⟩))
106102, 105mpd 15 . . 3 (πœ‘ β†’ (β—‘(π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©})β€˜{βŸ¨βˆ…, (𝐴 Β· 𝐡)⟩, ⟨1o, (𝐴 Γ— 𝐢)⟩}) = ⟨(𝐴 Β· 𝐡), (𝐴 Γ— 𝐢)⟩)
10798, 106eqtrd 2777 . 2 (πœ‘ β†’ (β—‘(π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©})β€˜(𝐴( ·𝑠 β€˜(𝐺Xs{βŸ¨βˆ…, π‘…βŸ©, ⟨1o, π‘†βŸ©})){βŸ¨βˆ…, 𝐡⟩, ⟨1o, 𝐢⟩})) = ⟨(𝐴 Β· 𝐡), (𝐴 Γ— 𝐢)⟩)
10841, 45, 1073eqtr3d 2785 1 (πœ‘ β†’ (𝐴 βˆ™ ⟨𝐡, 𝐢⟩) = ⟨(𝐴 Β· 𝐡), (𝐴 Γ— 𝐢)⟩)
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ∧ wa 397   = wceq 1542  βŠ€wtru 1543   ∈ wcel 2107  Vcvv 3446  βˆ…c0 4283  ifcif 4487  {cpr 4589  βŸ¨cop 4593   ↦ cmpt 5189   Γ— cxp 5632  β—‘ccnv 5633  ran crn 5635  Oncon0 6318   Fn wfn 6492  βŸΆwf 6493  β€“ontoβ†’wfo 6495  β€“1-1-ontoβ†’wf1o 6496  β€˜cfv 6497  (class class class)co 7358   ∈ cmpo 7360  1oc1o 8406  2oc2o 8407  Basecbs 17084  Scalarcsca 17137   ·𝑠 cvsca 17138  Xscprds 17328   Γ—s cxps 17389
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-rep 5243  ax-sep 5257  ax-nul 5264  ax-pow 5321  ax-pr 5385  ax-un 7673  ax-cnex 11108  ax-resscn 11109  ax-1cn 11110  ax-icn 11111  ax-addcl 11112  ax-addrcl 11113  ax-mulcl 11114  ax-mulrcl 11115  ax-mulcom 11116  ax-addass 11117  ax-mulass 11118  ax-distr 11119  ax-i2m1 11120  ax-1ne0 11121  ax-1rid 11122  ax-rnegex 11123  ax-rrecex 11124  ax-cnre 11125  ax-pre-lttri 11126  ax-pre-lttrn 11127  ax-pre-ltadd 11128  ax-pre-mulgt0 11129
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3066  df-rex 3075  df-reu 3355  df-rab 3409  df-v 3448  df-sbc 3741  df-csb 3857  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3930  df-nul 4284  df-if 4488  df-pw 4563  df-sn 4588  df-pr 4590  df-tp 4592  df-op 4594  df-uni 4867  df-iun 4957  df-br 5107  df-opab 5169  df-mpt 5190  df-tr 5224  df-id 5532  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5589  df-we 5591  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-pred 6254  df-ord 6321  df-on 6322  df-lim 6323  df-suc 6324  df-iota 6449  df-fun 6499  df-fn 6500  df-f 6501  df-f1 6502  df-fo 6503  df-f1o 6504  df-fv 6505  df-riota 7314  df-ov 7361  df-oprab 7362  df-mpo 7363  df-om 7804  df-1st 7922  df-2nd 7923  df-frecs 8213  df-wrecs 8244  df-recs 8318  df-rdg 8357  df-1o 8413  df-2o 8414  df-er 8649  df-map 8768  df-ixp 8837  df-en 8885  df-dom 8886  df-sdom 8887  df-fin 8888  df-sup 9379  df-inf 9380  df-pnf 11192  df-mnf 11193  df-xr 11194  df-ltxr 11195  df-le 11196  df-sub 11388  df-neg 11389  df-nn 12155  df-2 12217  df-3 12218  df-4 12219  df-5 12220  df-6 12221  df-7 12222  df-8 12223  df-9 12224  df-n0 12415  df-z 12501  df-dec 12620  df-uz 12765  df-fz 13426  df-struct 17020  df-slot 17055  df-ndx 17067  df-base 17085  df-plusg 17147  df-mulr 17148  df-sca 17150  df-vsca 17151  df-ip 17152  df-tset 17153  df-ple 17154  df-ds 17156  df-hom 17158  df-cco 17159  df-prds 17330  df-imas 17391  df-xps 17393
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator