Step | Hyp | Ref
| Expression |
1 | | xpsmnd.t |
. . 3
⊢ 𝑇 = (𝑅 ×s 𝑆) |
2 | | eqid 2610 |
. . 3
⊢
(Base‘𝑅) =
(Base‘𝑅) |
3 | | eqid 2610 |
. . 3
⊢
(Base‘𝑆) =
(Base‘𝑆) |
4 | | simpl 472 |
. . 3
⊢ ((𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd) → 𝑅 ∈ Mnd) |
5 | | simpr 476 |
. . 3
⊢ ((𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd) → 𝑆 ∈ Mnd) |
6 | | eqid 2610 |
. . 3
⊢ (𝑥 ∈ (Base‘𝑅), 𝑦 ∈ (Base‘𝑆) ↦ ◡({𝑥} +𝑐 {𝑦})) = (𝑥 ∈ (Base‘𝑅), 𝑦 ∈ (Base‘𝑆) ↦ ◡({𝑥} +𝑐 {𝑦})) |
7 | | eqid 2610 |
. . 3
⊢
(Scalar‘𝑅) =
(Scalar‘𝑅) |
8 | | eqid 2610 |
. . 3
⊢
((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆})) = ((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆})) |
9 | 1, 2, 3, 4, 5, 6, 7, 8 | xpsval 16055 |
. 2
⊢ ((𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd) → 𝑇 = (◡(𝑥 ∈ (Base‘𝑅), 𝑦 ∈ (Base‘𝑆) ↦ ◡({𝑥} +𝑐 {𝑦})) “s
((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆})))) |
10 | 6 | xpsff1o2 16054 |
. . . . 5
⊢ (𝑥 ∈ (Base‘𝑅), 𝑦 ∈ (Base‘𝑆) ↦ ◡({𝑥} +𝑐 {𝑦})):((Base‘𝑅) × (Base‘𝑆))–1-1-onto→ran
(𝑥 ∈ (Base‘𝑅), 𝑦 ∈ (Base‘𝑆) ↦ ◡({𝑥} +𝑐 {𝑦})) |
11 | 1, 2, 3, 4, 5, 6, 7, 8 | xpslem 16056 |
. . . . . 6
⊢ ((𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd) → ran (𝑥 ∈ (Base‘𝑅), 𝑦 ∈ (Base‘𝑆) ↦ ◡({𝑥} +𝑐 {𝑦})) = (Base‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆})))) |
12 | | f1oeq3 6042 |
. . . . . 6
⊢ (ran
(𝑥 ∈ (Base‘𝑅), 𝑦 ∈ (Base‘𝑆) ↦ ◡({𝑥} +𝑐 {𝑦})) = (Base‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆}))) → ((𝑥 ∈ (Base‘𝑅), 𝑦 ∈ (Base‘𝑆) ↦ ◡({𝑥} +𝑐 {𝑦})):((Base‘𝑅) × (Base‘𝑆))–1-1-onto→ran
(𝑥 ∈ (Base‘𝑅), 𝑦 ∈ (Base‘𝑆) ↦ ◡({𝑥} +𝑐 {𝑦})) ↔ (𝑥 ∈ (Base‘𝑅), 𝑦 ∈ (Base‘𝑆) ↦ ◡({𝑥} +𝑐 {𝑦})):((Base‘𝑅) × (Base‘𝑆))–1-1-onto→(Base‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆}))))) |
13 | 11, 12 | syl 17 |
. . . . 5
⊢ ((𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd) → ((𝑥 ∈ (Base‘𝑅), 𝑦 ∈ (Base‘𝑆) ↦ ◡({𝑥} +𝑐 {𝑦})):((Base‘𝑅) × (Base‘𝑆))–1-1-onto→ran
(𝑥 ∈ (Base‘𝑅), 𝑦 ∈ (Base‘𝑆) ↦ ◡({𝑥} +𝑐 {𝑦})) ↔ (𝑥 ∈ (Base‘𝑅), 𝑦 ∈ (Base‘𝑆) ↦ ◡({𝑥} +𝑐 {𝑦})):((Base‘𝑅) × (Base‘𝑆))–1-1-onto→(Base‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆}))))) |
14 | 10, 13 | mpbii 222 |
. . . 4
⊢ ((𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd) → (𝑥 ∈ (Base‘𝑅), 𝑦 ∈ (Base‘𝑆) ↦ ◡({𝑥} +𝑐 {𝑦})):((Base‘𝑅) × (Base‘𝑆))–1-1-onto→(Base‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆})))) |
15 | | f1ocnv 6062 |
. . . 4
⊢ ((𝑥 ∈ (Base‘𝑅), 𝑦 ∈ (Base‘𝑆) ↦ ◡({𝑥} +𝑐 {𝑦})):((Base‘𝑅) × (Base‘𝑆))–1-1-onto→(Base‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆}))) → ◡(𝑥 ∈ (Base‘𝑅), 𝑦 ∈ (Base‘𝑆) ↦ ◡({𝑥} +𝑐 {𝑦})):(Base‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆})))–1-1-onto→((Base‘𝑅) × (Base‘𝑆))) |
16 | | f1of1 6049 |
. . . 4
⊢ (◡(𝑥 ∈ (Base‘𝑅), 𝑦 ∈ (Base‘𝑆) ↦ ◡({𝑥} +𝑐 {𝑦})):(Base‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆})))–1-1-onto→((Base‘𝑅) × (Base‘𝑆)) → ◡(𝑥 ∈ (Base‘𝑅), 𝑦 ∈ (Base‘𝑆) ↦ ◡({𝑥} +𝑐 {𝑦})):(Base‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆})))–1-1→((Base‘𝑅) × (Base‘𝑆))) |
17 | 14, 15, 16 | 3syl 18 |
. . 3
⊢ ((𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd) → ◡(𝑥 ∈ (Base‘𝑅), 𝑦 ∈ (Base‘𝑆) ↦ ◡({𝑥} +𝑐 {𝑦})):(Base‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆})))–1-1→((Base‘𝑅) × (Base‘𝑆))) |
18 | | 2on 7455 |
. . . . 5
⊢
2𝑜 ∈ On |
19 | 18 | a1i 11 |
. . . 4
⊢ ((𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd) →
2𝑜 ∈ On) |
20 | | fvex 6113 |
. . . . 5
⊢
(Scalar‘𝑅)
∈ V |
21 | 20 | a1i 11 |
. . . 4
⊢ ((𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd) →
(Scalar‘𝑅) ∈
V) |
22 | | xpscf 16049 |
. . . . 5
⊢ (◡({𝑅} +𝑐 {𝑆}):2𝑜⟶Mnd ↔
(𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd)) |
23 | 22 | biimpri 217 |
. . . 4
⊢ ((𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd) → ◡({𝑅} +𝑐 {𝑆}):2𝑜⟶Mnd) |
24 | 8, 19, 21, 23 | prdsmndd 17146 |
. . 3
⊢ ((𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd) →
((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆})) ∈ Mnd) |
25 | | eqid 2610 |
. . . 4
⊢ (◡(𝑥 ∈ (Base‘𝑅), 𝑦 ∈ (Base‘𝑆) ↦ ◡({𝑥} +𝑐 {𝑦})) “s
((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆}))) = (◡(𝑥 ∈ (Base‘𝑅), 𝑦 ∈ (Base‘𝑆) ↦ ◡({𝑥} +𝑐 {𝑦})) “s
((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆}))) |
26 | | eqid 2610 |
. . . 4
⊢
(Base‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆}))) = (Base‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆}))) |
27 | 25, 26 | imasmndf1 17152 |
. . 3
⊢ ((◡(𝑥 ∈ (Base‘𝑅), 𝑦 ∈ (Base‘𝑆) ↦ ◡({𝑥} +𝑐 {𝑦})):(Base‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆})))–1-1→((Base‘𝑅) × (Base‘𝑆)) ∧ ((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆})) ∈ Mnd) → (◡(𝑥 ∈ (Base‘𝑅), 𝑦 ∈ (Base‘𝑆) ↦ ◡({𝑥} +𝑐 {𝑦})) “s
((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆}))) ∈ Mnd) |
28 | 17, 24, 27 | syl2anc 691 |
. 2
⊢ ((𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd) → (◡(𝑥 ∈ (Base‘𝑅), 𝑦 ∈ (Base‘𝑆) ↦ ◡({𝑥} +𝑐 {𝑦})) “s
((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆}))) ∈ Mnd) |
29 | 9, 28 | eqeltrd 2688 |
1
⊢ ((𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd) → 𝑇 ∈ Mnd) |