Step | Hyp | Ref
| Expression |
1 | | xpsmnd.t |
. . 3
⊢ 𝑇 = (𝑅 ×s 𝑆) |
2 | | eqid 2738 |
. . 3
⊢
(Base‘𝑅) =
(Base‘𝑅) |
3 | | eqid 2738 |
. . 3
⊢
(Base‘𝑆) =
(Base‘𝑆) |
4 | | simpl 483 |
. . 3
⊢ ((𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd) → 𝑅 ∈ Mnd) |
5 | | simpr 485 |
. . 3
⊢ ((𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd) → 𝑆 ∈ Mnd) |
6 | | eqid 2738 |
. . 3
⊢ (𝑥 ∈ (Base‘𝑅), 𝑦 ∈ (Base‘𝑆) ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉}) = (𝑥 ∈ (Base‘𝑅), 𝑦 ∈ (Base‘𝑆) ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉}) |
7 | | eqid 2738 |
. . 3
⊢
(Scalar‘𝑅) =
(Scalar‘𝑅) |
8 | | eqid 2738 |
. . 3
⊢
((Scalar‘𝑅)Xs{〈∅, 𝑅〉, 〈1o, 𝑆〉}) = ((Scalar‘𝑅)Xs{〈∅, 𝑅〉, 〈1o, 𝑆〉}) |
9 | 1, 2, 3, 4, 5, 6, 7, 8 | xpsval 17281 |
. 2
⊢ ((𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd) → 𝑇 = (◡(𝑥 ∈ (Base‘𝑅), 𝑦 ∈ (Base‘𝑆) ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉})
“s ((Scalar‘𝑅)Xs{〈∅, 𝑅〉, 〈1o, 𝑆〉}))) |
10 | 6 | xpsff1o2 17280 |
. . . . 5
⊢ (𝑥 ∈ (Base‘𝑅), 𝑦 ∈ (Base‘𝑆) ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉}):((Base‘𝑅) × (Base‘𝑆))–1-1-onto→ran
(𝑥 ∈ (Base‘𝑅), 𝑦 ∈ (Base‘𝑆) ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉}) |
11 | 1, 2, 3, 4, 5, 6, 7, 8 | xpsrnbas 17282 |
. . . . . 6
⊢ ((𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd) → ran (𝑥 ∈ (Base‘𝑅), 𝑦 ∈ (Base‘𝑆) ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉}) =
(Base‘((Scalar‘𝑅)Xs{〈∅, 𝑅〉, 〈1o, 𝑆〉}))) |
12 | 11 | f1oeq3d 6713 |
. . . . 5
⊢ ((𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd) → ((𝑥 ∈ (Base‘𝑅), 𝑦 ∈ (Base‘𝑆) ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉}):((Base‘𝑅) × (Base‘𝑆))–1-1-onto→ran
(𝑥 ∈ (Base‘𝑅), 𝑦 ∈ (Base‘𝑆) ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉}) ↔ (𝑥 ∈ (Base‘𝑅), 𝑦 ∈ (Base‘𝑆) ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉}):((Base‘𝑅) × (Base‘𝑆))–1-1-onto→(Base‘((Scalar‘𝑅)Xs{〈∅, 𝑅〉, 〈1o, 𝑆〉})))) |
13 | 10, 12 | mpbii 232 |
. . . 4
⊢ ((𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd) → (𝑥 ∈ (Base‘𝑅), 𝑦 ∈ (Base‘𝑆) ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉}):((Base‘𝑅) × (Base‘𝑆))–1-1-onto→(Base‘((Scalar‘𝑅)Xs{〈∅, 𝑅〉, 〈1o, 𝑆〉}))) |
14 | | f1ocnv 6728 |
. . . 4
⊢ ((𝑥 ∈ (Base‘𝑅), 𝑦 ∈ (Base‘𝑆) ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉}):((Base‘𝑅) × (Base‘𝑆))–1-1-onto→(Base‘((Scalar‘𝑅)Xs{〈∅, 𝑅〉, 〈1o, 𝑆〉})) → ◡(𝑥 ∈ (Base‘𝑅), 𝑦 ∈ (Base‘𝑆) ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉}):(Base‘((Scalar‘𝑅)Xs{〈∅, 𝑅〉, 〈1o, 𝑆〉}))–1-1-onto→((Base‘𝑅) × (Base‘𝑆))) |
15 | | f1of1 6715 |
. . . 4
⊢ (◡(𝑥 ∈ (Base‘𝑅), 𝑦 ∈ (Base‘𝑆) ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉}):(Base‘((Scalar‘𝑅)Xs{〈∅, 𝑅〉, 〈1o, 𝑆〉}))–1-1-onto→((Base‘𝑅) × (Base‘𝑆)) → ◡(𝑥 ∈ (Base‘𝑅), 𝑦 ∈ (Base‘𝑆) ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉}):(Base‘((Scalar‘𝑅)Xs{〈∅, 𝑅〉, 〈1o, 𝑆〉}))–1-1→((Base‘𝑅) × (Base‘𝑆))) |
16 | 13, 14, 15 | 3syl 18 |
. . 3
⊢ ((𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd) → ◡(𝑥 ∈ (Base‘𝑅), 𝑦 ∈ (Base‘𝑆) ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉}):(Base‘((Scalar‘𝑅)Xs{〈∅, 𝑅〉, 〈1o, 𝑆〉}))–1-1→((Base‘𝑅) × (Base‘𝑆))) |
17 | | 2on 8311 |
. . . . 5
⊢
2o ∈ On |
18 | 17 | a1i 11 |
. . . 4
⊢ ((𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd) →
2o ∈ On) |
19 | | fvexd 6789 |
. . . 4
⊢ ((𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd) →
(Scalar‘𝑅) ∈
V) |
20 | | xpscf 17276 |
. . . . 5
⊢
({〈∅, 𝑅〉, 〈1o, 𝑆〉}:2o⟶Mnd
↔ (𝑅 ∈ Mnd ∧
𝑆 ∈
Mnd)) |
21 | 20 | biimpri 227 |
. . . 4
⊢ ((𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd) →
{〈∅, 𝑅〉,
〈1o, 𝑆〉}:2o⟶Mnd) |
22 | 8, 18, 19, 21 | prdsmndd 18418 |
. . 3
⊢ ((𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd) →
((Scalar‘𝑅)Xs{〈∅, 𝑅〉, 〈1o,
𝑆〉}) ∈
Mnd) |
23 | | eqid 2738 |
. . . 4
⊢ (◡(𝑥 ∈ (Base‘𝑅), 𝑦 ∈ (Base‘𝑆) ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉})
“s ((Scalar‘𝑅)Xs{〈∅, 𝑅〉, 〈1o, 𝑆〉})) = (◡(𝑥 ∈ (Base‘𝑅), 𝑦 ∈ (Base‘𝑆) ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉})
“s ((Scalar‘𝑅)Xs{〈∅, 𝑅〉, 〈1o, 𝑆〉})) |
24 | | eqid 2738 |
. . . 4
⊢
(Base‘((Scalar‘𝑅)Xs{〈∅, 𝑅〉, 〈1o, 𝑆〉})) =
(Base‘((Scalar‘𝑅)Xs{〈∅, 𝑅〉, 〈1o, 𝑆〉})) |
25 | 23, 24 | imasmndf1 18424 |
. . 3
⊢ ((◡(𝑥 ∈ (Base‘𝑅), 𝑦 ∈ (Base‘𝑆) ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉}):(Base‘((Scalar‘𝑅)Xs{〈∅, 𝑅〉, 〈1o, 𝑆〉}))–1-1→((Base‘𝑅) × (Base‘𝑆)) ∧ ((Scalar‘𝑅)Xs{〈∅, 𝑅〉, 〈1o, 𝑆〉}) ∈ Mnd) →
(◡(𝑥 ∈ (Base‘𝑅), 𝑦 ∈ (Base‘𝑆) ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉})
“s ((Scalar‘𝑅)Xs{〈∅, 𝑅〉, 〈1o, 𝑆〉})) ∈
Mnd) |
26 | 16, 22, 25 | syl2anc 584 |
. 2
⊢ ((𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd) → (◡(𝑥 ∈ (Base‘𝑅), 𝑦 ∈ (Base‘𝑆) ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉})
“s ((Scalar‘𝑅)Xs{〈∅, 𝑅〉, 〈1o, 𝑆〉})) ∈
Mnd) |
27 | 9, 26 | eqeltrd 2839 |
1
⊢ ((𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd) → 𝑇 ∈ Mnd) |