| Step | Hyp | Ref
| Expression |
|---|
| 1 | | xpsmnd.t |
. . 3
⊢ 𝑇 = (𝑅 ×s 𝑆) |
| 2 | | eqid 2763 |
. . 3
⊢
(Base‘𝑅) =
(Base‘𝑅) |
| 3 | | eqid 2763 |
. . 3
⊢
(Base‘𝑆) =
(Base‘𝑆) |
| 4 | | simpl 488 |
. . 3
⊢ ((𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd) → 𝑅 ∈ Mnd) |
| 5 | | simpr 490 |
. . 3
⊢ ((𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd) → 𝑆 ∈ Mnd) |
| 6 | | eqid 2763 |
. . 3
⊢ (𝑥 ∈ (Base‘𝑅), 𝑦 ∈ (Base‘𝑆) ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}) = (𝑥 ∈ (Base‘𝑅), 𝑦 ∈ (Base‘𝑆) ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}) |
| 7 | | eqid 2763 |
. . 3
⊢
(Scalar‘𝑅) =
(Scalar‘𝑅) |
| 8 | | eqid 2763 |
. . 3
⊢
((Scalar‘𝑅)Xs{⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}) = ((Scalar‘𝑅)Xs{⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}) |
| 9 | 1, 2, 3, 4, 5, 6, 7, 8 | xpsval 17792 |
. 2
⊢ ((𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd) → 𝑇 = (◡(𝑥 ∈ (Base‘𝑅), 𝑦 ∈ (Base‘𝑆) ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})
“s ((Scalar‘𝑅)Xs{⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}))) |
| 10 | 6 | xpsff1o2 17791 |
. . . . 5
⊢ (𝑥 ∈ (Base‘𝑅), 𝑦 ∈ (Base‘𝑆) ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}):((Base‘𝑅) × (Base‘𝑆))⟶1-1ontoran (𝑥 ∈ (Base‘𝑅), 𝑦 ∈ (Base‘𝑆) ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}) |
| 11 | 1, 2, 3, 4, 5, 6, 7, 8 | xpsrnbas 17793 |
. . . . . 6
⊢ ((𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd) → ran (𝑥 ∈ (Base‘𝑅), 𝑦 ∈ (Base‘𝑆) ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}) =
(Base‘((Scalar‘𝑅)Xs{⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}))) |
| 12 | 11 | f1oeq3d 6851 |
. . . . 5
⊢ ((𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd) → ((𝑥 ∈ (Base‘𝑅), 𝑦 ∈ (Base‘𝑆) ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}):((Base‘𝑅) × (Base‘𝑆))⟶1-1ontoran (𝑥 ∈ (Base‘𝑅), 𝑦 ∈ (Base‘𝑆) ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}) ↔ (𝑥 ∈ (Base‘𝑅), 𝑦 ∈ (Base‘𝑆) ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}):((Base‘𝑅) × (Base‘𝑆))⟶1-1onto(Base‘((Scalar‘𝑅)Xs{⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩})))) |
| 13 | 10, 12 | mpbii 236 |
. . . 4
⊢ ((𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd) → (𝑥 ∈ (Base‘𝑅), 𝑦 ∈ (Base‘𝑆) ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}):((Base‘𝑅) × (Base‘𝑆))⟶1-1onto(Base‘((Scalar‘𝑅)Xs{⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}))) |
| 14 | | f1ocnv 6867 |
. . . 4
⊢ ((𝑥 ∈ (Base‘𝑅), 𝑦 ∈ (Base‘𝑆) ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}):((Base‘𝑅) × (Base‘𝑆))⟶1-1onto(Base‘((Scalar‘𝑅)Xs{⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩})) → ◡(𝑥 ∈ (Base‘𝑅), 𝑦 ∈ (Base‘𝑆) ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}):(Base‘((Scalar‘𝑅)Xs{⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}))⟶1-1onto((Base‘𝑅) × (Base‘𝑆))) |
| 15 | | f1of1 6853 |
. . . 4
⊢ (◡(𝑥 ∈ (Base‘𝑅), 𝑦 ∈ (Base‘𝑆) ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}):(Base‘((Scalar‘𝑅)Xs{⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}))⟶1-1onto((Base‘𝑅) × (Base‘𝑆)) → ◡(𝑥 ∈ (Base‘𝑅), 𝑦 ∈ (Base‘𝑆) ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}):(Base‘((Scalar‘𝑅)Xs{⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}))⟶1-1((Base‘𝑅) × (Base‘𝑆))) |
| 16 | 13, 14, 15 | 3syl 19 |
. . 3
⊢ ((𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd) → ◡(𝑥 ∈ (Base‘𝑅), 𝑦 ∈ (Base‘𝑆) ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}):(Base‘((Scalar‘𝑅)Xs{⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}))⟶1-1((Base‘𝑅) × (Base‘𝑆))) |
| 17 | | 2on 8528 |
. . . . 5
⊢
2o ∈ On |
| 18 | 17 | a1i 11 |
. . . 4
⊢ ((𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd) →
2o ∈ On) |
| 19 | | fvexd 6931 |
. . . 4
⊢ ((𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd) →
(Scalar‘𝑅) ∈
V) |
| 20 | | xpscf 17787 |
. . . . 5
⊢
({⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}:2o⟶Mnd
↔ (𝑅 ∈ Mnd ∧
𝑆 ∈
Mnd)) |
| 21 | 20 | biimpri 231 |
. . . 4
⊢ ((𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd) →
{⟨∅, 𝑅⟩,
⟨1o, 𝑆⟩}:2o⟶Mnd) |
| 22 | 8, 18, 19, 21 | prdsmndd 19014 |
. . 3
⊢ ((𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd) →
((Scalar‘𝑅)Xs{⟨∅, 𝑅⟩, ⟨1o,
𝑆⟩}) ∈
Mnd) |
| 23 | | eqid 2763 |
. . . 4
⊢ (◡(𝑥 ∈ (Base‘𝑅), 𝑦 ∈ (Base‘𝑆) ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})
“s ((Scalar‘𝑅)Xs{⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩})) = (◡(𝑥 ∈ (Base‘𝑅), 𝑦 ∈ (Base‘𝑆) ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})
“s ((Scalar‘𝑅)Xs{⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩})) |
| 24 | | eqid 2763 |
. . . 4
⊢
(Base‘((Scalar‘𝑅)Xs{⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩})) =
(Base‘((Scalar‘𝑅)Xs{⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩})) |
| 25 | 23, 24 | imasmndf1 19020 |
. . 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 596 |
. 2
⊢ ((𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd) → (◡(𝑥 ∈ (Base‘𝑅), 𝑦 ∈ (Base‘𝑆) ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})
“s ((Scalar‘𝑅)Xs{⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩})) ∈
Mnd) |
| 27 | 9, 26 | eqeltrd 2864 |
1
⊢ ((𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd) → 𝑇 ∈ Mnd) |
