Proof of Theorem cramer0
Step | Hyp | Ref
| Expression |
1 | | cramer.b |
. . . . . . . . 9
⊢ 𝐵 = (Base‘𝐴) |
2 | | cramer.a |
. . . . . . . . . 10
⊢ 𝐴 = (𝑁 Mat 𝑅) |
3 | 2 | fveq2i 6106 |
. . . . . . . . 9
⊢
(Base‘𝐴) =
(Base‘(𝑁 Mat 𝑅)) |
4 | 1, 3 | eqtri 2632 |
. . . . . . . 8
⊢ 𝐵 = (Base‘(𝑁 Mat 𝑅)) |
5 | | oveq1 6556 |
. . . . . . . . 9
⊢ (𝑁 = ∅ → (𝑁 Mat 𝑅) = (∅ Mat 𝑅)) |
6 | 5 | fveq2d 6107 |
. . . . . . . 8
⊢ (𝑁 = ∅ →
(Base‘(𝑁 Mat 𝑅)) = (Base‘(∅ Mat
𝑅))) |
7 | 4, 6 | syl5eq 2656 |
. . . . . . 7
⊢ (𝑁 = ∅ → 𝐵 = (Base‘(∅ Mat
𝑅))) |
8 | 7 | adantr 480 |
. . . . . 6
⊢ ((𝑁 = ∅ ∧ 𝑅 ∈ CRing) → 𝐵 = (Base‘(∅ Mat
𝑅))) |
9 | 8 | eleq2d 2673 |
. . . . 5
⊢ ((𝑁 = ∅ ∧ 𝑅 ∈ CRing) → (𝑋 ∈ 𝐵 ↔ 𝑋 ∈ (Base‘(∅ Mat 𝑅)))) |
10 | | mat0dimbas0 20091 |
. . . . . . 7
⊢ (𝑅 ∈ CRing →
(Base‘(∅ Mat 𝑅)) = {∅}) |
11 | 10 | eleq2d 2673 |
. . . . . 6
⊢ (𝑅 ∈ CRing → (𝑋 ∈ (Base‘(∅ Mat
𝑅)) ↔ 𝑋 ∈
{∅})) |
12 | 11 | adantl 481 |
. . . . 5
⊢ ((𝑁 = ∅ ∧ 𝑅 ∈ CRing) → (𝑋 ∈ (Base‘(∅ Mat
𝑅)) ↔ 𝑋 ∈
{∅})) |
13 | 9, 12 | bitrd 267 |
. . . 4
⊢ ((𝑁 = ∅ ∧ 𝑅 ∈ CRing) → (𝑋 ∈ 𝐵 ↔ 𝑋 ∈ {∅})) |
14 | | cramer.v |
. . . . . . . 8
⊢ 𝑉 = ((Base‘𝑅) ↑𝑚
𝑁) |
15 | 14 | a1i 11 |
. . . . . . 7
⊢ ((𝑁 = ∅ ∧ 𝑅 ∈ CRing) → 𝑉 = ((Base‘𝑅) ↑𝑚
𝑁)) |
16 | | oveq2 6557 |
. . . . . . . 8
⊢ (𝑁 = ∅ →
((Base‘𝑅)
↑𝑚 𝑁) = ((Base‘𝑅) ↑𝑚
∅)) |
17 | 16 | adantr 480 |
. . . . . . 7
⊢ ((𝑁 = ∅ ∧ 𝑅 ∈ CRing) →
((Base‘𝑅)
↑𝑚 𝑁) = ((Base‘𝑅) ↑𝑚
∅)) |
18 | | fvex 6113 |
. . . . . . . 8
⊢
(Base‘𝑅)
∈ V |
19 | | map0e 7781 |
. . . . . . . 8
⊢
((Base‘𝑅)
∈ V → ((Base‘𝑅) ↑𝑚 ∅) =
1𝑜) |
20 | 18, 19 | mp1i 13 |
. . . . . . 7
⊢ ((𝑁 = ∅ ∧ 𝑅 ∈ CRing) →
((Base‘𝑅)
↑𝑚 ∅) = 1𝑜) |
21 | 15, 17, 20 | 3eqtrd 2648 |
. . . . . 6
⊢ ((𝑁 = ∅ ∧ 𝑅 ∈ CRing) → 𝑉 =
1𝑜) |
22 | 21 | eleq2d 2673 |
. . . . 5
⊢ ((𝑁 = ∅ ∧ 𝑅 ∈ CRing) → (𝑌 ∈ 𝑉 ↔ 𝑌 ∈
1𝑜)) |
23 | | el1o 7466 |
. . . . 5
⊢ (𝑌 ∈ 1𝑜
↔ 𝑌 =
∅) |
24 | 22, 23 | syl6bb 275 |
. . . 4
⊢ ((𝑁 = ∅ ∧ 𝑅 ∈ CRing) → (𝑌 ∈ 𝑉 ↔ 𝑌 = ∅)) |
25 | 13, 24 | anbi12d 743 |
. . 3
⊢ ((𝑁 = ∅ ∧ 𝑅 ∈ CRing) → ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ↔ (𝑋 ∈ {∅} ∧ 𝑌 = ∅))) |
26 | | elsni 4142 |
. . . 4
⊢ (𝑋 ∈ {∅} → 𝑋 = ∅) |
27 | | mpteq1 4665 |
. . . . . . . . . 10
⊢ (𝑁 = ∅ → (𝑖 ∈ 𝑁 ↦ ((𝐷‘((𝑋(𝑁 matRepV 𝑅)𝑌)‘𝑖)) / (𝐷‘𝑋))) = (𝑖 ∈ ∅ ↦ ((𝐷‘((𝑋(𝑁 matRepV 𝑅)𝑌)‘𝑖)) / (𝐷‘𝑋)))) |
28 | | mpt0 5934 |
. . . . . . . . . 10
⊢ (𝑖 ∈ ∅ ↦ ((𝐷‘((𝑋(𝑁 matRepV 𝑅)𝑌)‘𝑖)) / (𝐷‘𝑋))) = ∅ |
29 | 27, 28 | syl6eq 2660 |
. . . . . . . . 9
⊢ (𝑁 = ∅ → (𝑖 ∈ 𝑁 ↦ ((𝐷‘((𝑋(𝑁 matRepV 𝑅)𝑌)‘𝑖)) / (𝐷‘𝑋))) = ∅) |
30 | 29 | eqeq2d 2620 |
. . . . . . . 8
⊢ (𝑁 = ∅ → (𝑍 = (𝑖 ∈ 𝑁 ↦ ((𝐷‘((𝑋(𝑁 matRepV 𝑅)𝑌)‘𝑖)) / (𝐷‘𝑋))) ↔ 𝑍 = ∅)) |
31 | 30 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝑁 = ∅ ∧ 𝑅 ∈ CRing) ∧ (𝑋 = ∅ ∧ 𝑌 = ∅)) → (𝑍 = (𝑖 ∈ 𝑁 ↦ ((𝐷‘((𝑋(𝑁 matRepV 𝑅)𝑌)‘𝑖)) / (𝐷‘𝑋))) ↔ 𝑍 = ∅)) |
32 | | simplrl 796 |
. . . . . . . . . 10
⊢ ((((𝑁 = ∅ ∧ 𝑅 ∈ CRing) ∧ (𝑋 = ∅ ∧ 𝑌 = ∅)) ∧ 𝑍 = ∅) → 𝑋 = ∅) |
33 | | simpr 476 |
. . . . . . . . . 10
⊢ ((((𝑁 = ∅ ∧ 𝑅 ∈ CRing) ∧ (𝑋 = ∅ ∧ 𝑌 = ∅)) ∧ 𝑍 = ∅) → 𝑍 = ∅) |
34 | 32, 33 | oveq12d 6567 |
. . . . . . . . 9
⊢ ((((𝑁 = ∅ ∧ 𝑅 ∈ CRing) ∧ (𝑋 = ∅ ∧ 𝑌 = ∅)) ∧ 𝑍 = ∅) → (𝑋 · 𝑍) = (∅ ·
∅)) |
35 | | cramer.x |
. . . . . . . . . . 11
⊢ · =
(𝑅 maVecMul 〈𝑁, 𝑁〉) |
36 | 35 | mavmul0 20177 |
. . . . . . . . . 10
⊢ ((𝑁 = ∅ ∧ 𝑅 ∈ CRing) → (∅
·
∅) = ∅) |
37 | 36 | ad2antrr 758 |
. . . . . . . . 9
⊢ ((((𝑁 = ∅ ∧ 𝑅 ∈ CRing) ∧ (𝑋 = ∅ ∧ 𝑌 = ∅)) ∧ 𝑍 = ∅) → (∅
·
∅) = ∅) |
38 | | simpr 476 |
. . . . . . . . . . 11
⊢ ((𝑋 = ∅ ∧ 𝑌 = ∅) → 𝑌 = ∅) |
39 | 38 | eqcomd 2616 |
. . . . . . . . . 10
⊢ ((𝑋 = ∅ ∧ 𝑌 = ∅) → ∅ =
𝑌) |
40 | 39 | ad2antlr 759 |
. . . . . . . . 9
⊢ ((((𝑁 = ∅ ∧ 𝑅 ∈ CRing) ∧ (𝑋 = ∅ ∧ 𝑌 = ∅)) ∧ 𝑍 = ∅) → ∅ =
𝑌) |
41 | 34, 37, 40 | 3eqtrd 2648 |
. . . . . . . 8
⊢ ((((𝑁 = ∅ ∧ 𝑅 ∈ CRing) ∧ (𝑋 = ∅ ∧ 𝑌 = ∅)) ∧ 𝑍 = ∅) → (𝑋 · 𝑍) = 𝑌) |
42 | 41 | ex 449 |
. . . . . . 7
⊢ (((𝑁 = ∅ ∧ 𝑅 ∈ CRing) ∧ (𝑋 = ∅ ∧ 𝑌 = ∅)) → (𝑍 = ∅ → (𝑋 · 𝑍) = 𝑌)) |
43 | 31, 42 | sylbid 229 |
. . . . . 6
⊢ (((𝑁 = ∅ ∧ 𝑅 ∈ CRing) ∧ (𝑋 = ∅ ∧ 𝑌 = ∅)) → (𝑍 = (𝑖 ∈ 𝑁 ↦ ((𝐷‘((𝑋(𝑁 matRepV 𝑅)𝑌)‘𝑖)) / (𝐷‘𝑋))) → (𝑋 · 𝑍) = 𝑌)) |
44 | 43 | a1d 25 |
. . . . 5
⊢ (((𝑁 = ∅ ∧ 𝑅 ∈ CRing) ∧ (𝑋 = ∅ ∧ 𝑌 = ∅)) → ((𝐷‘𝑋) ∈ (Unit‘𝑅) → (𝑍 = (𝑖 ∈ 𝑁 ↦ ((𝐷‘((𝑋(𝑁 matRepV 𝑅)𝑌)‘𝑖)) / (𝐷‘𝑋))) → (𝑋 · 𝑍) = 𝑌))) |
45 | 44 | ex 449 |
. . . 4
⊢ ((𝑁 = ∅ ∧ 𝑅 ∈ CRing) → ((𝑋 = ∅ ∧ 𝑌 = ∅) → ((𝐷‘𝑋) ∈ (Unit‘𝑅) → (𝑍 = (𝑖 ∈ 𝑁 ↦ ((𝐷‘((𝑋(𝑁 matRepV 𝑅)𝑌)‘𝑖)) / (𝐷‘𝑋))) → (𝑋 · 𝑍) = 𝑌)))) |
46 | 26, 45 | sylani 684 |
. . 3
⊢ ((𝑁 = ∅ ∧ 𝑅 ∈ CRing) → ((𝑋 ∈ {∅} ∧ 𝑌 = ∅) → ((𝐷‘𝑋) ∈ (Unit‘𝑅) → (𝑍 = (𝑖 ∈ 𝑁 ↦ ((𝐷‘((𝑋(𝑁 matRepV 𝑅)𝑌)‘𝑖)) / (𝐷‘𝑋))) → (𝑋 · 𝑍) = 𝑌)))) |
47 | 25, 46 | sylbid 229 |
. 2
⊢ ((𝑁 = ∅ ∧ 𝑅 ∈ CRing) → ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) → ((𝐷‘𝑋) ∈ (Unit‘𝑅) → (𝑍 = (𝑖 ∈ 𝑁 ↦ ((𝐷‘((𝑋(𝑁 matRepV 𝑅)𝑌)‘𝑖)) / (𝐷‘𝑋))) → (𝑋 · 𝑍) = 𝑌)))) |
48 | 47 | 3imp 1249 |
1
⊢ (((𝑁 = ∅ ∧ 𝑅 ∈ CRing) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝐷‘𝑋) ∈ (Unit‘𝑅)) → (𝑍 = (𝑖 ∈ 𝑁 ↦ ((𝐷‘((𝑋(𝑁 matRepV 𝑅)𝑌)‘𝑖)) / (𝐷‘𝑋))) → (𝑋 · 𝑍) = 𝑌)) |