Proof of Theorem slesolinvbi
Step | Hyp | Ref
| Expression |
1 | | simpl1 1190 |
. . 3
⊢ ((((𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝐷‘𝑋) ∈ (Unit‘𝑅)) ∧ (𝑋 · 𝑍) = 𝑌) → (𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing)) |
2 | | simpl2 1191 |
. . 3
⊢ ((((𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝐷‘𝑋) ∈ (Unit‘𝑅)) ∧ (𝑋 · 𝑍) = 𝑌) → (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉)) |
3 | | simp3 1137 |
. . . 4
⊢ (((𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝐷‘𝑋) ∈ (Unit‘𝑅)) → (𝐷‘𝑋) ∈ (Unit‘𝑅)) |
4 | 3 | anim1i 615 |
. . 3
⊢ ((((𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝐷‘𝑋) ∈ (Unit‘𝑅)) ∧ (𝑋 · 𝑍) = 𝑌) → ((𝐷‘𝑋) ∈ (Unit‘𝑅) ∧ (𝑋 · 𝑍) = 𝑌)) |
5 | | slesolex.a |
. . . 4
⊢ 𝐴 = (𝑁 Mat 𝑅) |
6 | | slesolex.b |
. . . 4
⊢ 𝐵 = (Base‘𝐴) |
7 | | slesolex.v |
. . . 4
⊢ 𝑉 = ((Base‘𝑅) ↑m 𝑁) |
8 | | slesolex.x |
. . . 4
⊢ · =
(𝑅 maVecMul 〈𝑁, 𝑁〉) |
9 | | slesolex.d |
. . . 4
⊢ 𝐷 = (𝑁 maDet 𝑅) |
10 | | slesolinv.i |
. . . 4
⊢ 𝐼 = (invr‘𝐴) |
11 | 5, 6, 7, 8, 9, 10 | slesolinv 21829 |
. . 3
⊢ (((𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ ((𝐷‘𝑋) ∈ (Unit‘𝑅) ∧ (𝑋 · 𝑍) = 𝑌)) → 𝑍 = ((𝐼‘𝑋) · 𝑌)) |
12 | 1, 2, 4, 11 | syl3anc 1370 |
. 2
⊢ ((((𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝐷‘𝑋) ∈ (Unit‘𝑅)) ∧ (𝑋 · 𝑍) = 𝑌) → 𝑍 = ((𝐼‘𝑋) · 𝑌)) |
13 | | oveq2 7283 |
. . 3
⊢ (𝑍 = ((𝐼‘𝑋) · 𝑌) → (𝑋 · 𝑍) = (𝑋 · ((𝐼‘𝑋) · 𝑌))) |
14 | | simpr 485 |
. . . . . . . . . 10
⊢ ((𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing) → 𝑅 ∈ CRing) |
15 | 5, 6 | matrcl 21559 |
. . . . . . . . . . . 12
⊢ (𝑋 ∈ 𝐵 → (𝑁 ∈ Fin ∧ 𝑅 ∈ V)) |
16 | 15 | simpld 495 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ 𝐵 → 𝑁 ∈ Fin) |
17 | 16 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) → 𝑁 ∈ Fin) |
18 | 14, 17 | anim12ci 614 |
. . . . . . . . 9
⊢ (((𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉)) → (𝑁 ∈ Fin ∧ 𝑅 ∈ CRing)) |
19 | 18 | 3adant3 1131 |
. . . . . . . 8
⊢ (((𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝐷‘𝑋) ∈ (Unit‘𝑅)) → (𝑁 ∈ Fin ∧ 𝑅 ∈ CRing)) |
20 | | eqid 2738 |
. . . . . . . . 9
⊢ (𝑅 maMul 〈𝑁, 𝑁, 𝑁〉) = (𝑅 maMul 〈𝑁, 𝑁, 𝑁〉) |
21 | 5, 20 | matmulr 21587 |
. . . . . . . 8
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (𝑅 maMul 〈𝑁, 𝑁, 𝑁〉) = (.r‘𝐴)) |
22 | 19, 21 | syl 17 |
. . . . . . 7
⊢ (((𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝐷‘𝑋) ∈ (Unit‘𝑅)) → (𝑅 maMul 〈𝑁, 𝑁, 𝑁〉) = (.r‘𝐴)) |
23 | 22 | oveqd 7292 |
. . . . . 6
⊢ (((𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝐷‘𝑋) ∈ (Unit‘𝑅)) → (𝑋(𝑅 maMul 〈𝑁, 𝑁, 𝑁〉)(𝐼‘𝑋)) = (𝑋(.r‘𝐴)(𝐼‘𝑋))) |
24 | | crngring 19795 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring) |
25 | 24 | adantl 482 |
. . . . . . . . . 10
⊢ ((𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing) → 𝑅 ∈ Ring) |
26 | 25, 17 | anim12ci 614 |
. . . . . . . . 9
⊢ (((𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉)) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring)) |
27 | 26 | 3adant3 1131 |
. . . . . . . 8
⊢ (((𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝐷‘𝑋) ∈ (Unit‘𝑅)) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring)) |
28 | 5 | matring 21592 |
. . . . . . . 8
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐴 ∈ Ring) |
29 | 27, 28 | syl 17 |
. . . . . . 7
⊢ (((𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝐷‘𝑋) ∈ (Unit‘𝑅)) → 𝐴 ∈ Ring) |
30 | | eqid 2738 |
. . . . . . . . . 10
⊢
(Unit‘𝐴) =
(Unit‘𝐴) |
31 | | eqid 2738 |
. . . . . . . . . 10
⊢
(Unit‘𝑅) =
(Unit‘𝑅) |
32 | 5, 9, 6, 30, 31 | matunit 21827 |
. . . . . . . . 9
⊢ ((𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵) → (𝑋 ∈ (Unit‘𝐴) ↔ (𝐷‘𝑋) ∈ (Unit‘𝑅))) |
33 | 32 | ad2ant2lr 745 |
. . . . . . . 8
⊢ (((𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉)) → (𝑋 ∈ (Unit‘𝐴) ↔ (𝐷‘𝑋) ∈ (Unit‘𝑅))) |
34 | 33 | biimp3ar 1469 |
. . . . . . 7
⊢ (((𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝐷‘𝑋) ∈ (Unit‘𝑅)) → 𝑋 ∈ (Unit‘𝐴)) |
35 | | eqid 2738 |
. . . . . . . 8
⊢
(.r‘𝐴) = (.r‘𝐴) |
36 | | eqid 2738 |
. . . . . . . 8
⊢
(1r‘𝐴) = (1r‘𝐴) |
37 | 30, 10, 35, 36 | unitrinv 19920 |
. . . . . . 7
⊢ ((𝐴 ∈ Ring ∧ 𝑋 ∈ (Unit‘𝐴)) → (𝑋(.r‘𝐴)(𝐼‘𝑋)) = (1r‘𝐴)) |
38 | 29, 34, 37 | syl2anc 584 |
. . . . . 6
⊢ (((𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝐷‘𝑋) ∈ (Unit‘𝑅)) → (𝑋(.r‘𝐴)(𝐼‘𝑋)) = (1r‘𝐴)) |
39 | 23, 38 | eqtrd 2778 |
. . . . 5
⊢ (((𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝐷‘𝑋) ∈ (Unit‘𝑅)) → (𝑋(𝑅 maMul 〈𝑁, 𝑁, 𝑁〉)(𝐼‘𝑋)) = (1r‘𝐴)) |
40 | 39 | oveq1d 7290 |
. . . 4
⊢ (((𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝐷‘𝑋) ∈ (Unit‘𝑅)) → ((𝑋(𝑅 maMul 〈𝑁, 𝑁, 𝑁〉)(𝐼‘𝑋)) · 𝑌) = ((1r‘𝐴) · 𝑌)) |
41 | | eqid 2738 |
. . . . 5
⊢
(Base‘𝑅) =
(Base‘𝑅) |
42 | 25 | 3ad2ant1 1132 |
. . . . 5
⊢ (((𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝐷‘𝑋) ∈ (Unit‘𝑅)) → 𝑅 ∈ Ring) |
43 | 17 | 3ad2ant2 1133 |
. . . . 5
⊢ (((𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝐷‘𝑋) ∈ (Unit‘𝑅)) → 𝑁 ∈ Fin) |
44 | 7 | eleq2i 2830 |
. . . . . . . 8
⊢ (𝑌 ∈ 𝑉 ↔ 𝑌 ∈ ((Base‘𝑅) ↑m 𝑁)) |
45 | 44 | biimpi 215 |
. . . . . . 7
⊢ (𝑌 ∈ 𝑉 → 𝑌 ∈ ((Base‘𝑅) ↑m 𝑁)) |
46 | 45 | adantl 482 |
. . . . . 6
⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) → 𝑌 ∈ ((Base‘𝑅) ↑m 𝑁)) |
47 | 46 | 3ad2ant2 1133 |
. . . . 5
⊢ (((𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝐷‘𝑋) ∈ (Unit‘𝑅)) → 𝑌 ∈ ((Base‘𝑅) ↑m 𝑁)) |
48 | 6 | eleq2i 2830 |
. . . . . . . 8
⊢ (𝑋 ∈ 𝐵 ↔ 𝑋 ∈ (Base‘𝐴)) |
49 | 48 | biimpi 215 |
. . . . . . 7
⊢ (𝑋 ∈ 𝐵 → 𝑋 ∈ (Base‘𝐴)) |
50 | 49 | adantr 481 |
. . . . . 6
⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) → 𝑋 ∈ (Base‘𝐴)) |
51 | 50 | 3ad2ant2 1133 |
. . . . 5
⊢ (((𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝐷‘𝑋) ∈ (Unit‘𝑅)) → 𝑋 ∈ (Base‘𝐴)) |
52 | | eqid 2738 |
. . . . . . 7
⊢
(Base‘𝐴) =
(Base‘𝐴) |
53 | 30, 10, 52 | ringinvcl 19918 |
. . . . . 6
⊢ ((𝐴 ∈ Ring ∧ 𝑋 ∈ (Unit‘𝐴)) → (𝐼‘𝑋) ∈ (Base‘𝐴)) |
54 | 29, 34, 53 | syl2anc 584 |
. . . . 5
⊢ (((𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝐷‘𝑋) ∈ (Unit‘𝑅)) → (𝐼‘𝑋) ∈ (Base‘𝐴)) |
55 | 5, 41, 8, 42, 43, 47, 20, 51, 54 | mavmulass 21698 |
. . . 4
⊢ (((𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝐷‘𝑋) ∈ (Unit‘𝑅)) → ((𝑋(𝑅 maMul 〈𝑁, 𝑁, 𝑁〉)(𝐼‘𝑋)) · 𝑌) = (𝑋 · ((𝐼‘𝑋) · 𝑌))) |
56 | 5, 41, 8, 42, 43, 47 | 1mavmul 21697 |
. . . 4
⊢ (((𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝐷‘𝑋) ∈ (Unit‘𝑅)) → ((1r‘𝐴) · 𝑌) = 𝑌) |
57 | 40, 55, 56 | 3eqtr3d 2786 |
. . 3
⊢ (((𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝐷‘𝑋) ∈ (Unit‘𝑅)) → (𝑋 · ((𝐼‘𝑋) · 𝑌)) = 𝑌) |
58 | 13, 57 | sylan9eqr 2800 |
. 2
⊢ ((((𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝐷‘𝑋) ∈ (Unit‘𝑅)) ∧ 𝑍 = ((𝐼‘𝑋) · 𝑌)) → (𝑋 · 𝑍) = 𝑌) |
59 | 12, 58 | impbida 798 |
1
⊢ (((𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝐷‘𝑋) ∈ (Unit‘𝑅)) → ((𝑋 · 𝑍) = 𝑌 ↔ 𝑍 = ((𝐼‘𝑋) · 𝑌))) |