| Step | Hyp | Ref
| Expression |
| 1 | | scmatid.e |
. . . . 5
⊢ 𝐸 = (Base‘𝑅) |
| 2 | | scmatid.a |
. . . . 5
⊢ 𝐴 = (𝑁 Mat 𝑅) |
| 3 | | scmatid.b |
. . . . 5
⊢ 𝐵 = (Base‘𝐴) |
| 4 | | eqid 2737 |
. . . . 5
⊢
(1r‘𝐴) = (1r‘𝐴) |
| 5 | | eqid 2737 |
. . . . 5
⊢ (
·𝑠 ‘𝐴) = ( ·𝑠
‘𝐴) |
| 6 | | scmatid.s |
. . . . 5
⊢ 𝑆 = (𝑁 ScMat 𝑅) |
| 7 | 1, 2, 3, 4, 5, 6 | scmatscmid 22512 |
. . . 4
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑆) → ∃𝑐 ∈ 𝐸 𝑋 = (𝑐( ·𝑠
‘𝐴)(1r‘𝐴))) |
| 8 | 7 | 3expa 1119 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑋 ∈ 𝑆) → ∃𝑐 ∈ 𝐸 𝑋 = (𝑐( ·𝑠
‘𝐴)(1r‘𝐴))) |
| 9 | 8 | adantrr 717 |
. 2
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆)) → ∃𝑐 ∈ 𝐸 𝑋 = (𝑐( ·𝑠
‘𝐴)(1r‘𝐴))) |
| 10 | 1, 2, 3, 4, 5, 6 | scmatscmid 22512 |
. . . . . 6
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑌 ∈ 𝑆) → ∃𝑑 ∈ 𝐸 𝑌 = (𝑑( ·𝑠
‘𝐴)(1r‘𝐴))) |
| 11 | 10 | 3expia 1122 |
. . . . 5
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝑌 ∈ 𝑆 → ∃𝑑 ∈ 𝐸 𝑌 = (𝑑( ·𝑠
‘𝐴)(1r‘𝐴)))) |
| 12 | | oveq12 7440 |
. . . . . . . . . . 11
⊢ ((𝑋 = (𝑐( ·𝑠
‘𝐴)(1r‘𝐴)) ∧ 𝑌 = (𝑑( ·𝑠
‘𝐴)(1r‘𝐴))) → (𝑋(-g‘𝐴)𝑌) = ((𝑐( ·𝑠
‘𝐴)(1r‘𝐴))(-g‘𝐴)(𝑑( ·𝑠
‘𝐴)(1r‘𝐴)))) |
| 13 | 12 | adantl 481 |
. . . . . . . . . 10
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝑑 ∈ 𝐸) ∧ 𝑐 ∈ 𝐸) ∧ (𝑋 = (𝑐( ·𝑠
‘𝐴)(1r‘𝐴)) ∧ 𝑌 = (𝑑( ·𝑠
‘𝐴)(1r‘𝐴)))) → (𝑋(-g‘𝐴)𝑌) = ((𝑐( ·𝑠
‘𝐴)(1r‘𝐴))(-g‘𝐴)(𝑑( ·𝑠
‘𝐴)(1r‘𝐴)))) |
| 14 | | eqid 2737 |
. . . . . . . . . . . . . 14
⊢
(Scalar‘𝐴) =
(Scalar‘𝐴) |
| 15 | | eqid 2737 |
. . . . . . . . . . . . . 14
⊢
(Base‘(Scalar‘𝐴)) = (Base‘(Scalar‘𝐴)) |
| 16 | | eqid 2737 |
. . . . . . . . . . . . . 14
⊢
(-g‘𝐴) = (-g‘𝐴) |
| 17 | | eqid 2737 |
. . . . . . . . . . . . . 14
⊢
(-g‘(Scalar‘𝐴)) =
(-g‘(Scalar‘𝐴)) |
| 18 | 2 | matlmod 22435 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐴 ∈ LMod) |
| 19 | 18 | ad2antrr 726 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑑 ∈ 𝐸) ∧ 𝑐 ∈ 𝐸) → 𝐴 ∈ LMod) |
| 20 | 2 | matsca2 22426 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑅 = (Scalar‘𝐴)) |
| 21 | 20 | fveq2d 6910 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) →
(Base‘𝑅) =
(Base‘(Scalar‘𝐴))) |
| 22 | 1, 21 | eqtrid 2789 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐸 =
(Base‘(Scalar‘𝐴))) |
| 23 | 22 | eleq2d 2827 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝑐 ∈ 𝐸 ↔ 𝑐 ∈ (Base‘(Scalar‘𝐴)))) |
| 24 | 23 | biimpd 229 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝑐 ∈ 𝐸 → 𝑐 ∈ (Base‘(Scalar‘𝐴)))) |
| 25 | 24 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑑 ∈ 𝐸) → (𝑐 ∈ 𝐸 → 𝑐 ∈ (Base‘(Scalar‘𝐴)))) |
| 26 | 25 | imp 406 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑑 ∈ 𝐸) ∧ 𝑐 ∈ 𝐸) → 𝑐 ∈ (Base‘(Scalar‘𝐴))) |
| 27 | 22 | eleq2d 2827 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝑑 ∈ 𝐸 ↔ 𝑑 ∈ (Base‘(Scalar‘𝐴)))) |
| 28 | 27 | biimpa 476 |
. . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑑 ∈ 𝐸) → 𝑑 ∈ (Base‘(Scalar‘𝐴))) |
| 29 | 28 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑑 ∈ 𝐸) ∧ 𝑐 ∈ 𝐸) → 𝑑 ∈ (Base‘(Scalar‘𝐴))) |
| 30 | 2 | matring 22449 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐴 ∈ Ring) |
| 31 | 3, 4 | ringidcl 20262 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ Ring →
(1r‘𝐴)
∈ 𝐵) |
| 32 | 30, 31 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) →
(1r‘𝐴)
∈ 𝐵) |
| 33 | 32 | ad2antrr 726 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑑 ∈ 𝐸) ∧ 𝑐 ∈ 𝐸) → (1r‘𝐴) ∈ 𝐵) |
| 34 | 3, 5, 14, 15, 16, 17, 19, 26, 29, 33 | lmodsubdir 20918 |
. . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑑 ∈ 𝐸) ∧ 𝑐 ∈ 𝐸) → ((𝑐(-g‘(Scalar‘𝐴))𝑑)( ·𝑠
‘𝐴)(1r‘𝐴)) = ((𝑐( ·𝑠
‘𝐴)(1r‘𝐴))(-g‘𝐴)(𝑑( ·𝑠
‘𝐴)(1r‘𝐴)))) |
| 35 | 34 | eqcomd 2743 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑑 ∈ 𝐸) ∧ 𝑐 ∈ 𝐸) → ((𝑐( ·𝑠
‘𝐴)(1r‘𝐴))(-g‘𝐴)(𝑑( ·𝑠
‘𝐴)(1r‘𝐴))) = ((𝑐(-g‘(Scalar‘𝐴))𝑑)( ·𝑠
‘𝐴)(1r‘𝐴))) |
| 36 | | simpll 767 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑑 ∈ 𝐸) ∧ 𝑐 ∈ 𝐸) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring)) |
| 37 | 20 | eqcomd 2743 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) →
(Scalar‘𝐴) = 𝑅) |
| 38 | 37 | ad2antrr 726 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑑 ∈ 𝐸) ∧ 𝑐 ∈ 𝐸) → (Scalar‘𝐴) = 𝑅) |
| 39 | 38 | fveq2d 6910 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑑 ∈ 𝐸) ∧ 𝑐 ∈ 𝐸) →
(-g‘(Scalar‘𝐴)) = (-g‘𝑅)) |
| 40 | 39 | oveqd 7448 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑑 ∈ 𝐸) ∧ 𝑐 ∈ 𝐸) → (𝑐(-g‘(Scalar‘𝐴))𝑑) = (𝑐(-g‘𝑅)𝑑)) |
| 41 | | ringgrp 20235 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp) |
| 42 | 41 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑅 ∈ Grp) |
| 43 | 42 | ad2antrr 726 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑑 ∈ 𝐸) ∧ 𝑐 ∈ 𝐸) → 𝑅 ∈ Grp) |
| 44 | | simpr 484 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑑 ∈ 𝐸) ∧ 𝑐 ∈ 𝐸) → 𝑐 ∈ 𝐸) |
| 45 | | simplr 769 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑑 ∈ 𝐸) ∧ 𝑐 ∈ 𝐸) → 𝑑 ∈ 𝐸) |
| 46 | | eqid 2737 |
. . . . . . . . . . . . . . . . 17
⊢
(-g‘𝑅) = (-g‘𝑅) |
| 47 | 1, 46 | grpsubcl 19038 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑅 ∈ Grp ∧ 𝑐 ∈ 𝐸 ∧ 𝑑 ∈ 𝐸) → (𝑐(-g‘𝑅)𝑑) ∈ 𝐸) |
| 48 | 43, 44, 45, 47 | syl3anc 1373 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑑 ∈ 𝐸) ∧ 𝑐 ∈ 𝐸) → (𝑐(-g‘𝑅)𝑑) ∈ 𝐸) |
| 49 | 40, 48 | eqeltrd 2841 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑑 ∈ 𝐸) ∧ 𝑐 ∈ 𝐸) → (𝑐(-g‘(Scalar‘𝐴))𝑑) ∈ 𝐸) |
| 50 | 1, 2, 3, 5 | matvscl 22437 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ ((𝑐(-g‘(Scalar‘𝐴))𝑑) ∈ 𝐸 ∧ (1r‘𝐴) ∈ 𝐵)) → ((𝑐(-g‘(Scalar‘𝐴))𝑑)( ·𝑠
‘𝐴)(1r‘𝐴)) ∈ 𝐵) |
| 51 | 36, 49, 33, 50 | syl12anc 837 |
. . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑑 ∈ 𝐸) ∧ 𝑐 ∈ 𝐸) → ((𝑐(-g‘(Scalar‘𝐴))𝑑)( ·𝑠
‘𝐴)(1r‘𝐴)) ∈ 𝐵) |
| 52 | | oveq1 7438 |
. . . . . . . . . . . . . . . 16
⊢ (𝑒 = (𝑐(-g‘(Scalar‘𝐴))𝑑) → (𝑒( ·𝑠
‘𝐴)(1r‘𝐴)) = ((𝑐(-g‘(Scalar‘𝐴))𝑑)( ·𝑠
‘𝐴)(1r‘𝐴))) |
| 53 | 52 | eqeq2d 2748 |
. . . . . . . . . . . . . . 15
⊢ (𝑒 = (𝑐(-g‘(Scalar‘𝐴))𝑑) → (((𝑐(-g‘(Scalar‘𝐴))𝑑)( ·𝑠
‘𝐴)(1r‘𝐴)) = (𝑒( ·𝑠
‘𝐴)(1r‘𝐴)) ↔ ((𝑐(-g‘(Scalar‘𝐴))𝑑)( ·𝑠
‘𝐴)(1r‘𝐴)) = ((𝑐(-g‘(Scalar‘𝐴))𝑑)( ·𝑠
‘𝐴)(1r‘𝐴)))) |
| 54 | 53 | adantl 481 |
. . . . . . . . . . . . . 14
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝑑 ∈ 𝐸) ∧ 𝑐 ∈ 𝐸) ∧ 𝑒 = (𝑐(-g‘(Scalar‘𝐴))𝑑)) → (((𝑐(-g‘(Scalar‘𝐴))𝑑)( ·𝑠
‘𝐴)(1r‘𝐴)) = (𝑒( ·𝑠
‘𝐴)(1r‘𝐴)) ↔ ((𝑐(-g‘(Scalar‘𝐴))𝑑)( ·𝑠
‘𝐴)(1r‘𝐴)) = ((𝑐(-g‘(Scalar‘𝐴))𝑑)( ·𝑠
‘𝐴)(1r‘𝐴)))) |
| 55 | | eqidd 2738 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑑 ∈ 𝐸) ∧ 𝑐 ∈ 𝐸) → ((𝑐(-g‘(Scalar‘𝐴))𝑑)( ·𝑠
‘𝐴)(1r‘𝐴)) = ((𝑐(-g‘(Scalar‘𝐴))𝑑)( ·𝑠
‘𝐴)(1r‘𝐴))) |
| 56 | 49, 54, 55 | rspcedvd 3624 |
. . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑑 ∈ 𝐸) ∧ 𝑐 ∈ 𝐸) → ∃𝑒 ∈ 𝐸 ((𝑐(-g‘(Scalar‘𝐴))𝑑)( ·𝑠
‘𝐴)(1r‘𝐴)) = (𝑒( ·𝑠
‘𝐴)(1r‘𝐴))) |
| 57 | 1, 2, 3, 4, 5, 6 | scmatel 22511 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (((𝑐(-g‘(Scalar‘𝐴))𝑑)( ·𝑠
‘𝐴)(1r‘𝐴)) ∈ 𝑆 ↔ (((𝑐(-g‘(Scalar‘𝐴))𝑑)( ·𝑠
‘𝐴)(1r‘𝐴)) ∈ 𝐵 ∧ ∃𝑒 ∈ 𝐸 ((𝑐(-g‘(Scalar‘𝐴))𝑑)( ·𝑠
‘𝐴)(1r‘𝐴)) = (𝑒( ·𝑠
‘𝐴)(1r‘𝐴))))) |
| 58 | 57 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑑 ∈ 𝐸) ∧ 𝑐 ∈ 𝐸) → (((𝑐(-g‘(Scalar‘𝐴))𝑑)( ·𝑠
‘𝐴)(1r‘𝐴)) ∈ 𝑆 ↔ (((𝑐(-g‘(Scalar‘𝐴))𝑑)( ·𝑠
‘𝐴)(1r‘𝐴)) ∈ 𝐵 ∧ ∃𝑒 ∈ 𝐸 ((𝑐(-g‘(Scalar‘𝐴))𝑑)( ·𝑠
‘𝐴)(1r‘𝐴)) = (𝑒( ·𝑠
‘𝐴)(1r‘𝐴))))) |
| 59 | 51, 56, 58 | mpbir2and 713 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑑 ∈ 𝐸) ∧ 𝑐 ∈ 𝐸) → ((𝑐(-g‘(Scalar‘𝐴))𝑑)( ·𝑠
‘𝐴)(1r‘𝐴)) ∈ 𝑆) |
| 60 | 35, 59 | eqeltrd 2841 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑑 ∈ 𝐸) ∧ 𝑐 ∈ 𝐸) → ((𝑐( ·𝑠
‘𝐴)(1r‘𝐴))(-g‘𝐴)(𝑑( ·𝑠
‘𝐴)(1r‘𝐴))) ∈ 𝑆) |
| 61 | 60 | adantr 480 |
. . . . . . . . . 10
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝑑 ∈ 𝐸) ∧ 𝑐 ∈ 𝐸) ∧ (𝑋 = (𝑐( ·𝑠
‘𝐴)(1r‘𝐴)) ∧ 𝑌 = (𝑑( ·𝑠
‘𝐴)(1r‘𝐴)))) → ((𝑐( ·𝑠
‘𝐴)(1r‘𝐴))(-g‘𝐴)(𝑑( ·𝑠
‘𝐴)(1r‘𝐴))) ∈ 𝑆) |
| 62 | 13, 61 | eqeltrd 2841 |
. . . . . . . . 9
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝑑 ∈ 𝐸) ∧ 𝑐 ∈ 𝐸) ∧ (𝑋 = (𝑐( ·𝑠
‘𝐴)(1r‘𝐴)) ∧ 𝑌 = (𝑑( ·𝑠
‘𝐴)(1r‘𝐴)))) → (𝑋(-g‘𝐴)𝑌) ∈ 𝑆) |
| 63 | 62 | exp32 420 |
. . . . . . . 8
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑑 ∈ 𝐸) ∧ 𝑐 ∈ 𝐸) → (𝑋 = (𝑐( ·𝑠
‘𝐴)(1r‘𝐴)) → (𝑌 = (𝑑( ·𝑠
‘𝐴)(1r‘𝐴)) → (𝑋(-g‘𝐴)𝑌) ∈ 𝑆))) |
| 64 | 63 | rexlimdva 3155 |
. . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑑 ∈ 𝐸) → (∃𝑐 ∈ 𝐸 𝑋 = (𝑐( ·𝑠
‘𝐴)(1r‘𝐴)) → (𝑌 = (𝑑( ·𝑠
‘𝐴)(1r‘𝐴)) → (𝑋(-g‘𝐴)𝑌) ∈ 𝑆))) |
| 65 | 64 | com23 86 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑑 ∈ 𝐸) → (𝑌 = (𝑑( ·𝑠
‘𝐴)(1r‘𝐴)) → (∃𝑐 ∈ 𝐸 𝑋 = (𝑐( ·𝑠
‘𝐴)(1r‘𝐴)) → (𝑋(-g‘𝐴)𝑌) ∈ 𝑆))) |
| 66 | 65 | rexlimdva 3155 |
. . . . 5
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) →
(∃𝑑 ∈ 𝐸 𝑌 = (𝑑( ·𝑠
‘𝐴)(1r‘𝐴)) → (∃𝑐 ∈ 𝐸 𝑋 = (𝑐( ·𝑠
‘𝐴)(1r‘𝐴)) → (𝑋(-g‘𝐴)𝑌) ∈ 𝑆))) |
| 67 | 11, 66 | syldc 48 |
. . . 4
⊢ (𝑌 ∈ 𝑆 → ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (∃𝑐 ∈ 𝐸 𝑋 = (𝑐( ·𝑠
‘𝐴)(1r‘𝐴)) → (𝑋(-g‘𝐴)𝑌) ∈ 𝑆))) |
| 68 | 67 | adantl 481 |
. . 3
⊢ ((𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆) → ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (∃𝑐 ∈ 𝐸 𝑋 = (𝑐( ·𝑠
‘𝐴)(1r‘𝐴)) → (𝑋(-g‘𝐴)𝑌) ∈ 𝑆))) |
| 69 | 68 | impcom 407 |
. 2
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆)) → (∃𝑐 ∈ 𝐸 𝑋 = (𝑐( ·𝑠
‘𝐴)(1r‘𝐴)) → (𝑋(-g‘𝐴)𝑌) ∈ 𝑆)) |
| 70 | 9, 69 | mpd 15 |
1
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆)) → (𝑋(-g‘𝐴)𝑌) ∈ 𝑆) |