Proof of Theorem mat1dimelbas
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | snfi 9084 | . . . 4
⊢ {𝐸} ∈ Fin | 
| 2 |  | simpl 482 | . . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) → 𝑅 ∈ Ring) | 
| 3 |  | mat1dim.a | . . . . . . 7
⊢ 𝐴 = ({𝐸} Mat 𝑅) | 
| 4 |  | mat1dim.b | . . . . . . 7
⊢ 𝐵 = (Base‘𝑅) | 
| 5 | 3, 4 | matbas2 22428 | . . . . . 6
⊢ (({𝐸} ∈ Fin ∧ 𝑅 ∈ Ring) → (𝐵 ↑m ({𝐸} × {𝐸})) = (Base‘𝐴)) | 
| 6 | 5 | eqcomd 2742 | . . . . 5
⊢ (({𝐸} ∈ Fin ∧ 𝑅 ∈ Ring) →
(Base‘𝐴) = (𝐵 ↑m ({𝐸} × {𝐸}))) | 
| 7 | 6 | eleq2d 2826 | . . . 4
⊢ (({𝐸} ∈ Fin ∧ 𝑅 ∈ Ring) → (𝑀 ∈ (Base‘𝐴) ↔ 𝑀 ∈ (𝐵 ↑m ({𝐸} × {𝐸})))) | 
| 8 | 1, 2, 7 | sylancr 587 | . . 3
⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) → (𝑀 ∈ (Base‘𝐴) ↔ 𝑀 ∈ (𝐵 ↑m ({𝐸} × {𝐸})))) | 
| 9 | 4 | fvexi 6919 | . . . 4
⊢ 𝐵 ∈ V | 
| 10 |  | snex 5435 | . . . . . 6
⊢ {𝐸} ∈ V | 
| 11 | 10, 10 | pm3.2i 470 | . . . . 5
⊢ ({𝐸} ∈ V ∧ {𝐸} ∈ V) | 
| 12 |  | xpexg 7771 | . . . . 5
⊢ (({𝐸} ∈ V ∧ {𝐸} ∈ V) → ({𝐸} × {𝐸}) ∈ V) | 
| 13 | 11, 12 | mp1i 13 | . . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) → ({𝐸} × {𝐸}) ∈ V) | 
| 14 |  | elmapg 8880 | . . . 4
⊢ ((𝐵 ∈ V ∧ ({𝐸} × {𝐸}) ∈ V) → (𝑀 ∈ (𝐵 ↑m ({𝐸} × {𝐸})) ↔ 𝑀:({𝐸} × {𝐸})⟶𝐵)) | 
| 15 | 9, 13, 14 | sylancr 587 | . . 3
⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) → (𝑀 ∈ (𝐵 ↑m ({𝐸} × {𝐸})) ↔ 𝑀:({𝐸} × {𝐸})⟶𝐵)) | 
| 16 | 8, 15 | bitrd 279 | . 2
⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) → (𝑀 ∈ (Base‘𝐴) ↔ 𝑀:({𝐸} × {𝐸})⟶𝐵)) | 
| 17 |  | xpsng 7158 | . . . . . . . 8
⊢ ((𝐸 ∈ 𝑉 ∧ 𝐸 ∈ 𝑉) → ({𝐸} × {𝐸}) = {〈𝐸, 𝐸〉}) | 
| 18 | 17 | anidms 566 | . . . . . . 7
⊢ (𝐸 ∈ 𝑉 → ({𝐸} × {𝐸}) = {〈𝐸, 𝐸〉}) | 
| 19 | 18 | adantl 481 | . . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) → ({𝐸} × {𝐸}) = {〈𝐸, 𝐸〉}) | 
| 20 | 19 | feq2d 6721 | . . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) → (𝑀:({𝐸} × {𝐸})⟶𝐵 ↔ 𝑀:{〈𝐸, 𝐸〉}⟶𝐵)) | 
| 21 |  | opex 5468 | . . . . . . 7
⊢
〈𝐸, 𝐸〉 ∈ V | 
| 22 | 21 | fsn2 7155 | . . . . . 6
⊢ (𝑀:{〈𝐸, 𝐸〉}⟶𝐵 ↔ ((𝑀‘〈𝐸, 𝐸〉) ∈ 𝐵 ∧ 𝑀 = {〈〈𝐸, 𝐸〉, (𝑀‘〈𝐸, 𝐸〉)〉})) | 
| 23 |  | risset 3232 | . . . . . . . . . 10
⊢ ((𝑀‘〈𝐸, 𝐸〉) ∈ 𝐵 ↔ ∃𝑟 ∈ 𝐵 𝑟 = (𝑀‘〈𝐸, 𝐸〉)) | 
| 24 |  | eqcom 2743 | . . . . . . . . . . 11
⊢ (𝑟 = (𝑀‘〈𝐸, 𝐸〉) ↔ (𝑀‘〈𝐸, 𝐸〉) = 𝑟) | 
| 25 | 24 | rexbii 3093 | . . . . . . . . . 10
⊢
(∃𝑟 ∈
𝐵 𝑟 = (𝑀‘〈𝐸, 𝐸〉) ↔ ∃𝑟 ∈ 𝐵 (𝑀‘〈𝐸, 𝐸〉) = 𝑟) | 
| 26 | 23, 25 | sylbb 219 | . . . . . . . . 9
⊢ ((𝑀‘〈𝐸, 𝐸〉) ∈ 𝐵 → ∃𝑟 ∈ 𝐵 (𝑀‘〈𝐸, 𝐸〉) = 𝑟) | 
| 27 | 26 | ad2antrl 728 | . . . . . . . 8
⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ ((𝑀‘〈𝐸, 𝐸〉) ∈ 𝐵 ∧ 𝑀 = {〈〈𝐸, 𝐸〉, (𝑀‘〈𝐸, 𝐸〉)〉})) → ∃𝑟 ∈ 𝐵 (𝑀‘〈𝐸, 𝐸〉) = 𝑟) | 
| 28 |  | eqeq1 2740 | . . . . . . . . . . . 12
⊢ (𝑀 = {〈〈𝐸, 𝐸〉, (𝑀‘〈𝐸, 𝐸〉)〉} → (𝑀 = {〈〈𝐸, 𝐸〉, 𝑟〉} ↔ {〈〈𝐸, 𝐸〉, (𝑀‘〈𝐸, 𝐸〉)〉} = {〈〈𝐸, 𝐸〉, 𝑟〉})) | 
| 29 |  | opex 5468 | . . . . . . . . . . . . . 14
⊢
〈〈𝐸, 𝐸〉, (𝑀‘〈𝐸, 𝐸〉)〉 ∈ V | 
| 30 |  | sneqbg 4842 | . . . . . . . . . . . . . 14
⊢
(〈〈𝐸,
𝐸〉, (𝑀‘〈𝐸, 𝐸〉)〉 ∈ V →
({〈〈𝐸, 𝐸〉, (𝑀‘〈𝐸, 𝐸〉)〉} = {〈〈𝐸, 𝐸〉, 𝑟〉} ↔ 〈〈𝐸, 𝐸〉, (𝑀‘〈𝐸, 𝐸〉)〉 = 〈〈𝐸, 𝐸〉, 𝑟〉)) | 
| 31 | 29, 30 | ax-mp 5 | . . . . . . . . . . . . 13
⊢
({〈〈𝐸,
𝐸〉, (𝑀‘〈𝐸, 𝐸〉)〉} = {〈〈𝐸, 𝐸〉, 𝑟〉} ↔ 〈〈𝐸, 𝐸〉, (𝑀‘〈𝐸, 𝐸〉)〉 = 〈〈𝐸, 𝐸〉, 𝑟〉) | 
| 32 |  | eqid 2736 | . . . . . . . . . . . . . 14
⊢
〈𝐸, 𝐸〉 = 〈𝐸, 𝐸〉 | 
| 33 |  | vex 3483 | . . . . . . . . . . . . . . 15
⊢ 𝑟 ∈ V | 
| 34 | 21, 33 | opth2 5484 | . . . . . . . . . . . . . 14
⊢
(〈〈𝐸,
𝐸〉, (𝑀‘〈𝐸, 𝐸〉)〉 = 〈〈𝐸, 𝐸〉, 𝑟〉 ↔ (〈𝐸, 𝐸〉 = 〈𝐸, 𝐸〉 ∧ (𝑀‘〈𝐸, 𝐸〉) = 𝑟)) | 
| 35 | 32, 34 | mpbiran 709 | . . . . . . . . . . . . 13
⊢
(〈〈𝐸,
𝐸〉, (𝑀‘〈𝐸, 𝐸〉)〉 = 〈〈𝐸, 𝐸〉, 𝑟〉 ↔ (𝑀‘〈𝐸, 𝐸〉) = 𝑟) | 
| 36 | 31, 35 | bitri 275 | . . . . . . . . . . . 12
⊢
({〈〈𝐸,
𝐸〉, (𝑀‘〈𝐸, 𝐸〉)〉} = {〈〈𝐸, 𝐸〉, 𝑟〉} ↔ (𝑀‘〈𝐸, 𝐸〉) = 𝑟) | 
| 37 | 28, 36 | bitrdi 287 | . . . . . . . . . . 11
⊢ (𝑀 = {〈〈𝐸, 𝐸〉, (𝑀‘〈𝐸, 𝐸〉)〉} → (𝑀 = {〈〈𝐸, 𝐸〉, 𝑟〉} ↔ (𝑀‘〈𝐸, 𝐸〉) = 𝑟)) | 
| 38 | 37 | adantl 481 | . . . . . . . . . 10
⊢ (((𝑀‘〈𝐸, 𝐸〉) ∈ 𝐵 ∧ 𝑀 = {〈〈𝐸, 𝐸〉, (𝑀‘〈𝐸, 𝐸〉)〉}) → (𝑀 = {〈〈𝐸, 𝐸〉, 𝑟〉} ↔ (𝑀‘〈𝐸, 𝐸〉) = 𝑟)) | 
| 39 | 38 | adantl 481 | . . . . . . . . 9
⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ ((𝑀‘〈𝐸, 𝐸〉) ∈ 𝐵 ∧ 𝑀 = {〈〈𝐸, 𝐸〉, (𝑀‘〈𝐸, 𝐸〉)〉})) → (𝑀 = {〈〈𝐸, 𝐸〉, 𝑟〉} ↔ (𝑀‘〈𝐸, 𝐸〉) = 𝑟)) | 
| 40 | 39 | rexbidv 3178 | . . . . . . . 8
⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ ((𝑀‘〈𝐸, 𝐸〉) ∈ 𝐵 ∧ 𝑀 = {〈〈𝐸, 𝐸〉, (𝑀‘〈𝐸, 𝐸〉)〉})) → (∃𝑟 ∈ 𝐵 𝑀 = {〈〈𝐸, 𝐸〉, 𝑟〉} ↔ ∃𝑟 ∈ 𝐵 (𝑀‘〈𝐸, 𝐸〉) = 𝑟)) | 
| 41 | 27, 40 | mpbird 257 | . . . . . . 7
⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ ((𝑀‘〈𝐸, 𝐸〉) ∈ 𝐵 ∧ 𝑀 = {〈〈𝐸, 𝐸〉, (𝑀‘〈𝐸, 𝐸〉)〉})) → ∃𝑟 ∈ 𝐵 𝑀 = {〈〈𝐸, 𝐸〉, 𝑟〉}) | 
| 42 | 41 | ex 412 | . . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) → (((𝑀‘〈𝐸, 𝐸〉) ∈ 𝐵 ∧ 𝑀 = {〈〈𝐸, 𝐸〉, (𝑀‘〈𝐸, 𝐸〉)〉}) → ∃𝑟 ∈ 𝐵 𝑀 = {〈〈𝐸, 𝐸〉, 𝑟〉})) | 
| 43 | 22, 42 | biimtrid 242 | . . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) → (𝑀:{〈𝐸, 𝐸〉}⟶𝐵 → ∃𝑟 ∈ 𝐵 𝑀 = {〈〈𝐸, 𝐸〉, 𝑟〉})) | 
| 44 | 20, 43 | sylbid 240 | . . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) → (𝑀:({𝐸} × {𝐸})⟶𝐵 → ∃𝑟 ∈ 𝐵 𝑀 = {〈〈𝐸, 𝐸〉, 𝑟〉})) | 
| 45 |  | f1o2sn 7161 | . . . . . . . . 9
⊢ ((𝐸 ∈ 𝑉 ∧ 𝑟 ∈ 𝐵) → {〈〈𝐸, 𝐸〉, 𝑟〉}:({𝐸} × {𝐸})–1-1-onto→{𝑟}) | 
| 46 |  | f1of 6847 | . . . . . . . . 9
⊢
({〈〈𝐸,
𝐸〉, 𝑟〉}:({𝐸} × {𝐸})–1-1-onto→{𝑟} → {〈〈𝐸, 𝐸〉, 𝑟〉}:({𝐸} × {𝐸})⟶{𝑟}) | 
| 47 | 45, 46 | syl 17 | . . . . . . . 8
⊢ ((𝐸 ∈ 𝑉 ∧ 𝑟 ∈ 𝐵) → {〈〈𝐸, 𝐸〉, 𝑟〉}:({𝐸} × {𝐸})⟶{𝑟}) | 
| 48 | 47 | adantll 714 | . . . . . . 7
⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ 𝑟 ∈ 𝐵) → {〈〈𝐸, 𝐸〉, 𝑟〉}:({𝐸} × {𝐸})⟶{𝑟}) | 
| 49 |  | snssi 4807 | . . . . . . . 8
⊢ (𝑟 ∈ 𝐵 → {𝑟} ⊆ 𝐵) | 
| 50 | 49 | adantl 481 | . . . . . . 7
⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ 𝑟 ∈ 𝐵) → {𝑟} ⊆ 𝐵) | 
| 51 | 48, 50 | fssd 6752 | . . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ 𝑟 ∈ 𝐵) → {〈〈𝐸, 𝐸〉, 𝑟〉}:({𝐸} × {𝐸})⟶𝐵) | 
| 52 |  | feq1 6715 | . . . . . 6
⊢ (𝑀 = {〈〈𝐸, 𝐸〉, 𝑟〉} → (𝑀:({𝐸} × {𝐸})⟶𝐵 ↔ {〈〈𝐸, 𝐸〉, 𝑟〉}:({𝐸} × {𝐸})⟶𝐵)) | 
| 53 | 51, 52 | syl5ibrcom 247 | . . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ 𝑟 ∈ 𝐵) → (𝑀 = {〈〈𝐸, 𝐸〉, 𝑟〉} → 𝑀:({𝐸} × {𝐸})⟶𝐵)) | 
| 54 | 53 | rexlimdva 3154 | . . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) → (∃𝑟 ∈ 𝐵 𝑀 = {〈〈𝐸, 𝐸〉, 𝑟〉} → 𝑀:({𝐸} × {𝐸})⟶𝐵)) | 
| 55 | 44, 54 | impbid 212 | . . 3
⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) → (𝑀:({𝐸} × {𝐸})⟶𝐵 ↔ ∃𝑟 ∈ 𝐵 𝑀 = {〈〈𝐸, 𝐸〉, 𝑟〉})) | 
| 56 |  | mat1dim.o | . . . . . . . . 9
⊢ 𝑂 = 〈𝐸, 𝐸〉 | 
| 57 | 56 | eqcomi 2745 | . . . . . . . 8
⊢
〈𝐸, 𝐸〉 = 𝑂 | 
| 58 | 57 | opeq1i 4875 | . . . . . . 7
⊢
〈〈𝐸, 𝐸〉, 𝑟〉 = 〈𝑂, 𝑟〉 | 
| 59 | 58 | sneqi 4636 | . . . . . 6
⊢
{〈〈𝐸,
𝐸〉, 𝑟〉} = {〈𝑂, 𝑟〉} | 
| 60 | 59 | eqeq2i 2749 | . . . . 5
⊢ (𝑀 = {〈〈𝐸, 𝐸〉, 𝑟〉} ↔ 𝑀 = {〈𝑂, 𝑟〉}) | 
| 61 | 60 | a1i 11 | . . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) → (𝑀 = {〈〈𝐸, 𝐸〉, 𝑟〉} ↔ 𝑀 = {〈𝑂, 𝑟〉})) | 
| 62 | 61 | rexbidv 3178 | . . 3
⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) → (∃𝑟 ∈ 𝐵 𝑀 = {〈〈𝐸, 𝐸〉, 𝑟〉} ↔ ∃𝑟 ∈ 𝐵 𝑀 = {〈𝑂, 𝑟〉})) | 
| 63 | 55, 62 | bitrd 279 | . 2
⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) → (𝑀:({𝐸} × {𝐸})⟶𝐵 ↔ ∃𝑟 ∈ 𝐵 𝑀 = {〈𝑂, 𝑟〉})) | 
| 64 | 16, 63 | bitrd 279 | 1
⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) → (𝑀 ∈ (Base‘𝐴) ↔ ∃𝑟 ∈ 𝐵 𝑀 = {〈𝑂, 𝑟〉})) |