| Step | Hyp | Ref
| Expression |
| 1 | | eqid 2737 |
. . . . 5
⊢
{〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊) ∧ ∃𝑡 ∈ 𝑆 (𝑡 · (((1st
‘𝑎) ·
(2nd ‘𝑏))
−
((1st ‘𝑏)
·
(2nd ‘𝑎)))) = 0 )} = {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊) ∧ ∃𝑡 ∈ 𝑆 (𝑡 · (((1st
‘𝑎) ·
(2nd ‘𝑏))
−
((1st ‘𝑏)
·
(2nd ‘𝑎)))) = 0 )} |
| 2 | 1 | relopabiv 5830 |
. . . 4
⊢ Rel
{〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊) ∧ ∃𝑡 ∈ 𝑆 (𝑡 · (((1st
‘𝑎) ·
(2nd ‘𝑏))
−
((1st ‘𝑏)
·
(2nd ‘𝑎)))) = 0 )} |
| 3 | 2 | a1i 11 |
. . 3
⊢ (𝜑 → Rel {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊) ∧ ∃𝑡 ∈ 𝑆 (𝑡 · (((1st
‘𝑎) ·
(2nd ‘𝑏))
−
((1st ‘𝑏)
·
(2nd ‘𝑎)))) = 0 )}) |
| 4 | | erler.q |
. . . . 5
⊢ ∼ =
(𝑅 ~RL
𝑆) |
| 5 | | erler.1 |
. . . . . 6
⊢ 𝐵 = (Base‘𝑅) |
| 6 | | erler.2 |
. . . . . 6
⊢ 0 =
(0g‘𝑅) |
| 7 | | erler.4 |
. . . . . 6
⊢ · =
(.r‘𝑅) |
| 8 | | erler.5 |
. . . . . 6
⊢ − =
(-g‘𝑅) |
| 9 | | erler.w |
. . . . . 6
⊢ 𝑊 = (𝐵 × 𝑆) |
| 10 | | erler.s |
. . . . . . 7
⊢ (𝜑 → 𝑆 ∈ (SubMnd‘(mulGrp‘𝑅))) |
| 11 | | eqid 2737 |
. . . . . . . . 9
⊢
(mulGrp‘𝑅) =
(mulGrp‘𝑅) |
| 12 | 11, 5 | mgpbas 20142 |
. . . . . . . 8
⊢ 𝐵 =
(Base‘(mulGrp‘𝑅)) |
| 13 | 12 | submss 18822 |
. . . . . . 7
⊢ (𝑆 ∈
(SubMnd‘(mulGrp‘𝑅)) → 𝑆 ⊆ 𝐵) |
| 14 | 10, 13 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑆 ⊆ 𝐵) |
| 15 | 5, 6, 7, 8, 9, 1, 14 | erlval 33262 |
. . . . 5
⊢ (𝜑 → (𝑅 ~RL 𝑆) = {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊) ∧ ∃𝑡 ∈ 𝑆 (𝑡 · (((1st
‘𝑎) ·
(2nd ‘𝑏))
−
((1st ‘𝑏)
·
(2nd ‘𝑎)))) = 0 )}) |
| 16 | 4, 15 | eqtrid 2789 |
. . . 4
⊢ (𝜑 → ∼ = {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊) ∧ ∃𝑡 ∈ 𝑆 (𝑡 · (((1st
‘𝑎) ·
(2nd ‘𝑏))
−
((1st ‘𝑏)
·
(2nd ‘𝑎)))) = 0 )}) |
| 17 | 16 | releqd 5788 |
. . 3
⊢ (𝜑 → (Rel ∼ ↔ Rel
{〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊) ∧ ∃𝑡 ∈ 𝑆 (𝑡 · (((1st
‘𝑎) ·
(2nd ‘𝑏))
−
((1st ‘𝑏)
·
(2nd ‘𝑎)))) = 0 )})) |
| 18 | 3, 17 | mpbird 257 |
. 2
⊢ (𝜑 → Rel ∼ ) |
| 19 | | simpl 482 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 = 𝑥 ∧ 𝑏 = 𝑦) → 𝑎 = 𝑥) |
| 20 | 19 | fveq2d 6910 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 = 𝑥 ∧ 𝑏 = 𝑦) → (1st ‘𝑎) = (1st ‘𝑥)) |
| 21 | | simpr 484 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 = 𝑥 ∧ 𝑏 = 𝑦) → 𝑏 = 𝑦) |
| 22 | 21 | fveq2d 6910 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 = 𝑥 ∧ 𝑏 = 𝑦) → (2nd ‘𝑏) = (2nd ‘𝑦)) |
| 23 | 20, 22 | oveq12d 7449 |
. . . . . . . . . . . . 13
⊢ ((𝑎 = 𝑥 ∧ 𝑏 = 𝑦) → ((1st ‘𝑎) · (2nd
‘𝑏)) =
((1st ‘𝑥)
·
(2nd ‘𝑦))) |
| 24 | 21 | fveq2d 6910 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 = 𝑥 ∧ 𝑏 = 𝑦) → (1st ‘𝑏) = (1st ‘𝑦)) |
| 25 | 19 | fveq2d 6910 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 = 𝑥 ∧ 𝑏 = 𝑦) → (2nd ‘𝑎) = (2nd ‘𝑥)) |
| 26 | 24, 25 | oveq12d 7449 |
. . . . . . . . . . . . 13
⊢ ((𝑎 = 𝑥 ∧ 𝑏 = 𝑦) → ((1st ‘𝑏) · (2nd
‘𝑎)) =
((1st ‘𝑦)
·
(2nd ‘𝑥))) |
| 27 | 23, 26 | oveq12d 7449 |
. . . . . . . . . . . 12
⊢ ((𝑎 = 𝑥 ∧ 𝑏 = 𝑦) → (((1st ‘𝑎) · (2nd
‘𝑏)) −
((1st ‘𝑏)
·
(2nd ‘𝑎)))
= (((1st ‘𝑥) · (2nd
‘𝑦)) −
((1st ‘𝑦)
·
(2nd ‘𝑥)))) |
| 28 | 27 | oveq2d 7447 |
. . . . . . . . . . 11
⊢ ((𝑎 = 𝑥 ∧ 𝑏 = 𝑦) → (𝑡 · (((1st
‘𝑎) ·
(2nd ‘𝑏))
−
((1st ‘𝑏)
·
(2nd ‘𝑎)))) = (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥))))) |
| 29 | 28 | eqeq1d 2739 |
. . . . . . . . . 10
⊢ ((𝑎 = 𝑥 ∧ 𝑏 = 𝑦) → ((𝑡 · (((1st
‘𝑎) ·
(2nd ‘𝑏))
−
((1st ‘𝑏)
·
(2nd ‘𝑎)))) = 0 ↔ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 )) |
| 30 | 29 | rexbidv 3179 |
. . . . . . . . 9
⊢ ((𝑎 = 𝑥 ∧ 𝑏 = 𝑦) → (∃𝑡 ∈ 𝑆 (𝑡 · (((1st
‘𝑎) ·
(2nd ‘𝑏))
−
((1st ‘𝑏)
·
(2nd ‘𝑎)))) = 0 ↔ ∃𝑡 ∈ 𝑆 (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 )) |
| 31 | 30 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑎 = 𝑥 ∧ 𝑏 = 𝑦)) → (∃𝑡 ∈ 𝑆 (𝑡 · (((1st
‘𝑎) ·
(2nd ‘𝑏))
−
((1st ‘𝑏)
·
(2nd ‘𝑎)))) = 0 ↔ ∃𝑡 ∈ 𝑆 (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 )) |
| 32 | 16, 31 | brab2d 32619 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∼ 𝑦 ↔ ((𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊) ∧ ∃𝑡 ∈ 𝑆 (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ))) |
| 33 | 32 | biimpa 476 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∼ 𝑦) → ((𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊) ∧ ∃𝑡 ∈ 𝑆 (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 )) |
| 34 | 33 | simplrd 770 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∼ 𝑦) → 𝑦 ∈ 𝑊) |
| 35 | 33 | simplld 768 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∼ 𝑦) → 𝑥 ∈ 𝑊) |
| 36 | 34, 35 | jca 511 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∼ 𝑦) → (𝑦 ∈ 𝑊 ∧ 𝑥 ∈ 𝑊)) |
| 37 | 33 | simprd 495 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∼ 𝑦) → ∃𝑡 ∈ 𝑆 (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) |
| 38 | | erler.r |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑅 ∈ CRing) |
| 39 | 38 | crngringd 20243 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑅 ∈ Ring) |
| 40 | 39 | ringgrpd 20239 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑅 ∈ Grp) |
| 41 | 40 | ad3antrrr 730 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) → 𝑅 ∈ Grp) |
| 42 | 39 | ad3antrrr 730 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) → 𝑅 ∈ Ring) |
| 43 | 35 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) → 𝑥 ∈ 𝑊) |
| 44 | | xp1st 8046 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (𝐵 × 𝑆) → (1st ‘𝑥) ∈ 𝐵) |
| 45 | 44, 9 | eleq2s 2859 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝑊 → (1st ‘𝑥) ∈ 𝐵) |
| 46 | 43, 45 | syl 17 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) → (1st
‘𝑥) ∈ 𝐵) |
| 47 | 14 | ad3antrrr 730 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) → 𝑆 ⊆ 𝐵) |
| 48 | 34 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) → 𝑦 ∈ 𝑊) |
| 49 | | xp2nd 8047 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ (𝐵 × 𝑆) → (2nd ‘𝑦) ∈ 𝑆) |
| 50 | 49, 9 | eleq2s 2859 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ 𝑊 → (2nd ‘𝑦) ∈ 𝑆) |
| 51 | 48, 50 | syl 17 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) → (2nd
‘𝑦) ∈ 𝑆) |
| 52 | 47, 51 | sseldd 3984 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) → (2nd
‘𝑦) ∈ 𝐵) |
| 53 | 5, 7, 42, 46, 52 | ringcld 20257 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) → ((1st
‘𝑥) ·
(2nd ‘𝑦))
∈ 𝐵) |
| 54 | | xp1st 8046 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ (𝐵 × 𝑆) → (1st ‘𝑦) ∈ 𝐵) |
| 55 | 54, 9 | eleq2s 2859 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ 𝑊 → (1st ‘𝑦) ∈ 𝐵) |
| 56 | 48, 55 | syl 17 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) → (1st
‘𝑦) ∈ 𝐵) |
| 57 | | xp2nd 8047 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ (𝐵 × 𝑆) → (2nd ‘𝑥) ∈ 𝑆) |
| 58 | 57, 9 | eleq2s 2859 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ 𝑊 → (2nd ‘𝑥) ∈ 𝑆) |
| 59 | 43, 58 | syl 17 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) → (2nd
‘𝑥) ∈ 𝑆) |
| 60 | 47, 59 | sseldd 3984 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) → (2nd
‘𝑥) ∈ 𝐵) |
| 61 | 5, 7, 42, 56, 60 | ringcld 20257 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) → ((1st
‘𝑦) ·
(2nd ‘𝑥))
∈ 𝐵) |
| 62 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(invg‘𝑅) = (invg‘𝑅) |
| 63 | 5, 8, 62 | grpinvsub 19040 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Grp ∧
((1st ‘𝑥)
·
(2nd ‘𝑦))
∈ 𝐵 ∧
((1st ‘𝑦)
·
(2nd ‘𝑥))
∈ 𝐵) →
((invg‘𝑅)‘(((1st ‘𝑥) · (2nd
‘𝑦)) −
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = (((1st ‘𝑦) · (2nd
‘𝑥)) −
((1st ‘𝑥)
·
(2nd ‘𝑦)))) |
| 64 | 41, 53, 61, 63 | syl3anc 1373 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) →
((invg‘𝑅)‘(((1st ‘𝑥) · (2nd
‘𝑦)) −
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = (((1st ‘𝑦) · (2nd
‘𝑥)) −
((1st ‘𝑥)
·
(2nd ‘𝑦)))) |
| 65 | 64 | oveq2d 7447 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) → (𝑡 ·
((invg‘𝑅)‘(((1st ‘𝑥) · (2nd
‘𝑦)) −
((1st ‘𝑦)
·
(2nd ‘𝑥))))) = (𝑡 · (((1st
‘𝑦) ·
(2nd ‘𝑥))
−
((1st ‘𝑥)
·
(2nd ‘𝑦))))) |
| 66 | | simplr 769 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) → 𝑡 ∈ 𝑆) |
| 67 | 47, 66 | sseldd 3984 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) → 𝑡 ∈ 𝐵) |
| 68 | 5, 8 | grpsubcl 19038 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ Grp ∧
((1st ‘𝑥)
·
(2nd ‘𝑦))
∈ 𝐵 ∧
((1st ‘𝑦)
·
(2nd ‘𝑥))
∈ 𝐵) →
(((1st ‘𝑥)
·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))
∈ 𝐵) |
| 69 | 41, 53, 61, 68 | syl3anc 1373 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) → (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))
∈ 𝐵) |
| 70 | 5, 7, 62, 42, 67, 69 | ringmneg2 20302 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) → (𝑡 ·
((invg‘𝑅)‘(((1st ‘𝑥) · (2nd
‘𝑦)) −
((1st ‘𝑦)
·
(2nd ‘𝑥))))) = ((invg‘𝑅)‘(𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))))) |
| 71 | | simpr 484 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) → (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) |
| 72 | 71 | fveq2d 6910 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) →
((invg‘𝑅)‘(𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥))))) = ((invg‘𝑅)‘ 0 )) |
| 73 | 6, 62 | grpinvid 19017 |
. . . . . . . . . 10
⊢ (𝑅 ∈ Grp →
((invg‘𝑅)‘ 0 ) = 0 ) |
| 74 | 41, 73 | syl 17 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) →
((invg‘𝑅)‘ 0 ) = 0 ) |
| 75 | 70, 72, 74 | 3eqtrd 2781 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) → (𝑡 ·
((invg‘𝑅)‘(((1st ‘𝑥) · (2nd
‘𝑦)) −
((1st ‘𝑦)
·
(2nd ‘𝑥))))) = 0 ) |
| 76 | 65, 75 | eqtr3d 2779 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) → (𝑡 · (((1st
‘𝑦) ·
(2nd ‘𝑥))
−
((1st ‘𝑥)
·
(2nd ‘𝑦)))) = 0 ) |
| 77 | 76 | ex 412 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑡 ∈ 𝑆) → ((𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 → (𝑡 · (((1st
‘𝑦) ·
(2nd ‘𝑥))
−
((1st ‘𝑥)
·
(2nd ‘𝑦)))) = 0 )) |
| 78 | 77 | reximdva 3168 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∼ 𝑦) → (∃𝑡 ∈ 𝑆 (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 → ∃𝑡 ∈ 𝑆 (𝑡 · (((1st
‘𝑦) ·
(2nd ‘𝑥))
−
((1st ‘𝑥)
·
(2nd ‘𝑦)))) = 0 )) |
| 79 | 37, 78 | mpd 15 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∼ 𝑦) → ∃𝑡 ∈ 𝑆 (𝑡 · (((1st
‘𝑦) ·
(2nd ‘𝑥))
−
((1st ‘𝑥)
·
(2nd ‘𝑦)))) = 0 ) |
| 80 | 36, 79 | jca 511 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∼ 𝑦) → ((𝑦 ∈ 𝑊 ∧ 𝑥 ∈ 𝑊) ∧ ∃𝑡 ∈ 𝑆 (𝑡 · (((1st
‘𝑦) ·
(2nd ‘𝑥))
−
((1st ‘𝑥)
·
(2nd ‘𝑦)))) = 0 )) |
| 81 | | simpl 482 |
. . . . . . . . . . . 12
⊢ ((𝑎 = 𝑦 ∧ 𝑏 = 𝑥) → 𝑎 = 𝑦) |
| 82 | 81 | fveq2d 6910 |
. . . . . . . . . . 11
⊢ ((𝑎 = 𝑦 ∧ 𝑏 = 𝑥) → (1st ‘𝑎) = (1st ‘𝑦)) |
| 83 | | simpr 484 |
. . . . . . . . . . . 12
⊢ ((𝑎 = 𝑦 ∧ 𝑏 = 𝑥) → 𝑏 = 𝑥) |
| 84 | 83 | fveq2d 6910 |
. . . . . . . . . . 11
⊢ ((𝑎 = 𝑦 ∧ 𝑏 = 𝑥) → (2nd ‘𝑏) = (2nd ‘𝑥)) |
| 85 | 82, 84 | oveq12d 7449 |
. . . . . . . . . 10
⊢ ((𝑎 = 𝑦 ∧ 𝑏 = 𝑥) → ((1st ‘𝑎) · (2nd
‘𝑏)) =
((1st ‘𝑦)
·
(2nd ‘𝑥))) |
| 86 | 83 | fveq2d 6910 |
. . . . . . . . . . 11
⊢ ((𝑎 = 𝑦 ∧ 𝑏 = 𝑥) → (1st ‘𝑏) = (1st ‘𝑥)) |
| 87 | 81 | fveq2d 6910 |
. . . . . . . . . . 11
⊢ ((𝑎 = 𝑦 ∧ 𝑏 = 𝑥) → (2nd ‘𝑎) = (2nd ‘𝑦)) |
| 88 | 86, 87 | oveq12d 7449 |
. . . . . . . . . 10
⊢ ((𝑎 = 𝑦 ∧ 𝑏 = 𝑥) → ((1st ‘𝑏) · (2nd
‘𝑎)) =
((1st ‘𝑥)
·
(2nd ‘𝑦))) |
| 89 | 85, 88 | oveq12d 7449 |
. . . . . . . . 9
⊢ ((𝑎 = 𝑦 ∧ 𝑏 = 𝑥) → (((1st ‘𝑎) · (2nd
‘𝑏)) −
((1st ‘𝑏)
·
(2nd ‘𝑎)))
= (((1st ‘𝑦) · (2nd
‘𝑥)) −
((1st ‘𝑥)
·
(2nd ‘𝑦)))) |
| 90 | 89 | oveq2d 7447 |
. . . . . . . 8
⊢ ((𝑎 = 𝑦 ∧ 𝑏 = 𝑥) → (𝑡 · (((1st
‘𝑎) ·
(2nd ‘𝑏))
−
((1st ‘𝑏)
·
(2nd ‘𝑎)))) = (𝑡 · (((1st
‘𝑦) ·
(2nd ‘𝑥))
−
((1st ‘𝑥)
·
(2nd ‘𝑦))))) |
| 91 | 90 | eqeq1d 2739 |
. . . . . . 7
⊢ ((𝑎 = 𝑦 ∧ 𝑏 = 𝑥) → ((𝑡 · (((1st
‘𝑎) ·
(2nd ‘𝑏))
−
((1st ‘𝑏)
·
(2nd ‘𝑎)))) = 0 ↔ (𝑡 · (((1st
‘𝑦) ·
(2nd ‘𝑥))
−
((1st ‘𝑥)
·
(2nd ‘𝑦)))) = 0 )) |
| 92 | 91 | rexbidv 3179 |
. . . . . 6
⊢ ((𝑎 = 𝑦 ∧ 𝑏 = 𝑥) → (∃𝑡 ∈ 𝑆 (𝑡 · (((1st
‘𝑎) ·
(2nd ‘𝑏))
−
((1st ‘𝑏)
·
(2nd ‘𝑎)))) = 0 ↔ ∃𝑡 ∈ 𝑆 (𝑡 · (((1st
‘𝑦) ·
(2nd ‘𝑥))
−
((1st ‘𝑥)
·
(2nd ‘𝑦)))) = 0 )) |
| 93 | 92 | adantl 481 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 = 𝑦 ∧ 𝑏 = 𝑥)) → (∃𝑡 ∈ 𝑆 (𝑡 · (((1st
‘𝑎) ·
(2nd ‘𝑏))
−
((1st ‘𝑏)
·
(2nd ‘𝑎)))) = 0 ↔ ∃𝑡 ∈ 𝑆 (𝑡 · (((1st
‘𝑦) ·
(2nd ‘𝑥))
−
((1st ‘𝑥)
·
(2nd ‘𝑦)))) = 0 )) |
| 94 | 16, 93 | brab2d 32619 |
. . . 4
⊢ (𝜑 → (𝑦 ∼ 𝑥 ↔ ((𝑦 ∈ 𝑊 ∧ 𝑥 ∈ 𝑊) ∧ ∃𝑡 ∈ 𝑆 (𝑡 · (((1st
‘𝑦) ·
(2nd ‘𝑥))
−
((1st ‘𝑥)
·
(2nd ‘𝑦)))) = 0 ))) |
| 95 | 94 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∼ 𝑦) → (𝑦 ∼ 𝑥 ↔ ((𝑦 ∈ 𝑊 ∧ 𝑥 ∈ 𝑊) ∧ ∃𝑡 ∈ 𝑆 (𝑡 · (((1st
‘𝑦) ·
(2nd ‘𝑥))
−
((1st ‘𝑥)
·
(2nd ‘𝑦)))) = 0 ))) |
| 96 | 80, 95 | mpbird 257 |
. 2
⊢ ((𝜑 ∧ 𝑥 ∼ 𝑦) → 𝑦 ∼ 𝑥) |
| 97 | 10 | ad6antr 736 |
. . . . . . 7
⊢
(((((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑦 ∼ 𝑧) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) ∧ 𝑢 ∈ 𝑆) ∧ (𝑢 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))) = 0 ) → 𝑆 ∈ (SubMnd‘(mulGrp‘𝑅))) |
| 98 | 97, 13 | syl 17 |
. . . . . 6
⊢
(((((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑦 ∼ 𝑧) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) ∧ 𝑢 ∈ 𝑆) ∧ (𝑢 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))) = 0 ) → 𝑆 ⊆ 𝐵) |
| 99 | 35 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑦 ∼ 𝑧) → 𝑥 ∈ 𝑊) |
| 100 | 99 | ad4antr 732 |
. . . . . . . 8
⊢
(((((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑦 ∼ 𝑧) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) ∧ 𝑢 ∈ 𝑆) ∧ (𝑢 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))) = 0 ) → 𝑥 ∈ 𝑊) |
| 101 | 100, 9 | eleqtrdi 2851 |
. . . . . . 7
⊢
(((((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑦 ∼ 𝑧) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) ∧ 𝑢 ∈ 𝑆) ∧ (𝑢 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))) = 0 ) → 𝑥 ∈ (𝐵 × 𝑆)) |
| 102 | | 1st2nd2 8053 |
. . . . . . 7
⊢ (𝑥 ∈ (𝐵 × 𝑆) → 𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉) |
| 103 | 101, 102 | syl 17 |
. . . . . 6
⊢
(((((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑦 ∼ 𝑧) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) ∧ 𝑢 ∈ 𝑆) ∧ (𝑢 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))) = 0 ) → 𝑥 = 〈(1st
‘𝑥), (2nd
‘𝑥)〉) |
| 104 | | simpl 482 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑎 = 𝑦 ∧ 𝑏 = 𝑧) → 𝑎 = 𝑦) |
| 105 | 104 | fveq2d 6910 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑎 = 𝑦 ∧ 𝑏 = 𝑧) → (1st ‘𝑎) = (1st ‘𝑦)) |
| 106 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑎 = 𝑦 ∧ 𝑏 = 𝑧) → 𝑏 = 𝑧) |
| 107 | 106 | fveq2d 6910 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑎 = 𝑦 ∧ 𝑏 = 𝑧) → (2nd ‘𝑏) = (2nd ‘𝑧)) |
| 108 | 105, 107 | oveq12d 7449 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑎 = 𝑦 ∧ 𝑏 = 𝑧) → ((1st ‘𝑎) · (2nd
‘𝑏)) =
((1st ‘𝑦)
·
(2nd ‘𝑧))) |
| 109 | 106 | fveq2d 6910 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑎 = 𝑦 ∧ 𝑏 = 𝑧) → (1st ‘𝑏) = (1st ‘𝑧)) |
| 110 | 104 | fveq2d 6910 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑎 = 𝑦 ∧ 𝑏 = 𝑧) → (2nd ‘𝑎) = (2nd ‘𝑦)) |
| 111 | 109, 110 | oveq12d 7449 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑎 = 𝑦 ∧ 𝑏 = 𝑧) → ((1st ‘𝑏) · (2nd
‘𝑎)) =
((1st ‘𝑧)
·
(2nd ‘𝑦))) |
| 112 | 108, 111 | oveq12d 7449 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑎 = 𝑦 ∧ 𝑏 = 𝑧) → (((1st ‘𝑎) · (2nd
‘𝑏)) −
((1st ‘𝑏)
·
(2nd ‘𝑎)))
= (((1st ‘𝑦) · (2nd
‘𝑧)) −
((1st ‘𝑧)
·
(2nd ‘𝑦)))) |
| 113 | 112 | oveq2d 7447 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑎 = 𝑦 ∧ 𝑏 = 𝑧) → (𝑡 · (((1st
‘𝑎) ·
(2nd ‘𝑏))
−
((1st ‘𝑏)
·
(2nd ‘𝑎)))) = (𝑡 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦))))) |
| 114 | 113 | eqeq1d 2739 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑎 = 𝑦 ∧ 𝑏 = 𝑧) → ((𝑡 · (((1st
‘𝑎) ·
(2nd ‘𝑏))
−
((1st ‘𝑏)
·
(2nd ‘𝑎)))) = 0 ↔ (𝑡 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))) = 0 )) |
| 115 | 114 | rexbidv 3179 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 = 𝑦 ∧ 𝑏 = 𝑧) → (∃𝑡 ∈ 𝑆 (𝑡 · (((1st
‘𝑎) ·
(2nd ‘𝑏))
−
((1st ‘𝑏)
·
(2nd ‘𝑎)))) = 0 ↔ ∃𝑡 ∈ 𝑆 (𝑡 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))) = 0 )) |
| 116 | | oveq1 7438 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑡 = 𝑢 → (𝑡 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))) = (𝑢 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦))))) |
| 117 | 116 | eqeq1d 2739 |
. . . . . . . . . . . . . . . 16
⊢ (𝑡 = 𝑢 → ((𝑡 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))) = 0 ↔ (𝑢 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))) = 0 )) |
| 118 | 117 | cbvrexvw 3238 |
. . . . . . . . . . . . . . 15
⊢
(∃𝑡 ∈
𝑆 (𝑡 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))) = 0 ↔ ∃𝑢 ∈ 𝑆 (𝑢 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))) = 0 ) |
| 119 | 115, 118 | bitrdi 287 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 = 𝑦 ∧ 𝑏 = 𝑧) → (∃𝑡 ∈ 𝑆 (𝑡 · (((1st
‘𝑎) ·
(2nd ‘𝑏))
−
((1st ‘𝑏)
·
(2nd ‘𝑎)))) = 0 ↔ ∃𝑢 ∈ 𝑆 (𝑢 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))) = 0 )) |
| 120 | 119 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑎 = 𝑦 ∧ 𝑏 = 𝑧)) → (∃𝑡 ∈ 𝑆 (𝑡 · (((1st
‘𝑎) ·
(2nd ‘𝑏))
−
((1st ‘𝑏)
·
(2nd ‘𝑎)))) = 0 ↔ ∃𝑢 ∈ 𝑆 (𝑢 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))) = 0 )) |
| 121 | 16, 120 | brab2d 32619 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑦 ∼ 𝑧 ↔ ((𝑦 ∈ 𝑊 ∧ 𝑧 ∈ 𝑊) ∧ ∃𝑢 ∈ 𝑆 (𝑢 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))) = 0 ))) |
| 122 | 121 | biimpa 476 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∼ 𝑧) → ((𝑦 ∈ 𝑊 ∧ 𝑧 ∈ 𝑊) ∧ ∃𝑢 ∈ 𝑆 (𝑢 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))) = 0 )) |
| 123 | 122 | adantlr 715 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑦 ∼ 𝑧) → ((𝑦 ∈ 𝑊 ∧ 𝑧 ∈ 𝑊) ∧ ∃𝑢 ∈ 𝑆 (𝑢 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))) = 0 )) |
| 124 | 123 | simplrd 770 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑦 ∼ 𝑧) → 𝑧 ∈ 𝑊) |
| 125 | 124 | ad4antr 732 |
. . . . . . . 8
⊢
(((((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑦 ∼ 𝑧) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) ∧ 𝑢 ∈ 𝑆) ∧ (𝑢 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))) = 0 ) → 𝑧 ∈ 𝑊) |
| 126 | 125, 9 | eleqtrdi 2851 |
. . . . . . 7
⊢
(((((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑦 ∼ 𝑧) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) ∧ 𝑢 ∈ 𝑆) ∧ (𝑢 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))) = 0 ) → 𝑧 ∈ (𝐵 × 𝑆)) |
| 127 | | 1st2nd2 8053 |
. . . . . . 7
⊢ (𝑧 ∈ (𝐵 × 𝑆) → 𝑧 = 〈(1st ‘𝑧), (2nd ‘𝑧)〉) |
| 128 | 126, 127 | syl 17 |
. . . . . 6
⊢
(((((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑦 ∼ 𝑧) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) ∧ 𝑢 ∈ 𝑆) ∧ (𝑢 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))) = 0 ) → 𝑧 = 〈(1st
‘𝑧), (2nd
‘𝑧)〉) |
| 129 | 100, 45 | syl 17 |
. . . . . 6
⊢
(((((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑦 ∼ 𝑧) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) ∧ 𝑢 ∈ 𝑆) ∧ (𝑢 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))) = 0 ) → (1st
‘𝑥) ∈ 𝐵) |
| 130 | | xp1st 8046 |
. . . . . . . 8
⊢ (𝑧 ∈ (𝐵 × 𝑆) → (1st ‘𝑧) ∈ 𝐵) |
| 131 | 130, 9 | eleq2s 2859 |
. . . . . . 7
⊢ (𝑧 ∈ 𝑊 → (1st ‘𝑧) ∈ 𝐵) |
| 132 | 125, 131 | syl 17 |
. . . . . 6
⊢
(((((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑦 ∼ 𝑧) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) ∧ 𝑢 ∈ 𝑆) ∧ (𝑢 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))) = 0 ) → (1st
‘𝑧) ∈ 𝐵) |
| 133 | 100, 58 | syl 17 |
. . . . . 6
⊢
(((((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑦 ∼ 𝑧) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) ∧ 𝑢 ∈ 𝑆) ∧ (𝑢 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))) = 0 ) → (2nd
‘𝑥) ∈ 𝑆) |
| 134 | | xp2nd 8047 |
. . . . . . . 8
⊢ (𝑧 ∈ (𝐵 × 𝑆) → (2nd ‘𝑧) ∈ 𝑆) |
| 135 | 134, 9 | eleq2s 2859 |
. . . . . . 7
⊢ (𝑧 ∈ 𝑊 → (2nd ‘𝑧) ∈ 𝑆) |
| 136 | 125, 135 | syl 17 |
. . . . . 6
⊢
(((((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑦 ∼ 𝑧) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) ∧ 𝑢 ∈ 𝑆) ∧ (𝑢 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))) = 0 ) → (2nd
‘𝑧) ∈ 𝑆) |
| 137 | | simp-4r 784 |
. . . . . . . 8
⊢
(((((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑦 ∼ 𝑧) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) ∧ 𝑢 ∈ 𝑆) ∧ (𝑢 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))) = 0 ) → 𝑡 ∈ 𝑆) |
| 138 | | simplr 769 |
. . . . . . . 8
⊢
(((((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑦 ∼ 𝑧) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) ∧ 𝑢 ∈ 𝑆) ∧ (𝑢 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))) = 0 ) → 𝑢 ∈ 𝑆) |
| 139 | 11, 7 | mgpplusg 20141 |
. . . . . . . . 9
⊢ · =
(+g‘(mulGrp‘𝑅)) |
| 140 | 139 | submcl 18825 |
. . . . . . . 8
⊢ ((𝑆 ∈
(SubMnd‘(mulGrp‘𝑅)) ∧ 𝑡 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆) → (𝑡 · 𝑢) ∈ 𝑆) |
| 141 | 97, 137, 138, 140 | syl3anc 1373 |
. . . . . . 7
⊢
(((((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑦 ∼ 𝑧) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) ∧ 𝑢 ∈ 𝑆) ∧ (𝑢 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))) = 0 ) → (𝑡 · 𝑢) ∈ 𝑆) |
| 142 | 34 | ad5antr 734 |
. . . . . . . 8
⊢
(((((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑦 ∼ 𝑧) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) ∧ 𝑢 ∈ 𝑆) ∧ (𝑢 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))) = 0 ) → 𝑦 ∈ 𝑊) |
| 143 | 142, 50 | syl 17 |
. . . . . . 7
⊢
(((((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑦 ∼ 𝑧) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) ∧ 𝑢 ∈ 𝑆) ∧ (𝑢 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))) = 0 ) → (2nd
‘𝑦) ∈ 𝑆) |
| 144 | 139 | submcl 18825 |
. . . . . . 7
⊢ ((𝑆 ∈
(SubMnd‘(mulGrp‘𝑅)) ∧ (𝑡 · 𝑢) ∈ 𝑆 ∧ (2nd ‘𝑦) ∈ 𝑆) → ((𝑡 · 𝑢) · (2nd
‘𝑦)) ∈ 𝑆) |
| 145 | 97, 141, 143, 144 | syl3anc 1373 |
. . . . . 6
⊢
(((((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑦 ∼ 𝑧) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) ∧ 𝑢 ∈ 𝑆) ∧ (𝑢 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))) = 0 ) → ((𝑡 · 𝑢) · (2nd
‘𝑦)) ∈ 𝑆) |
| 146 | 39 | ad6antr 736 |
. . . . . . . . . . 11
⊢
(((((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑦 ∼ 𝑧) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) ∧ 𝑢 ∈ 𝑆) ∧ (𝑢 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))) = 0 ) → 𝑅 ∈ Ring) |
| 147 | 98, 143 | sseldd 3984 |
. . . . . . . . . . 11
⊢
(((((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑦 ∼ 𝑧) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) ∧ 𝑢 ∈ 𝑆) ∧ (𝑢 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))) = 0 ) → (2nd
‘𝑦) ∈ 𝐵) |
| 148 | 98, 136 | sseldd 3984 |
. . . . . . . . . . . 12
⊢
(((((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑦 ∼ 𝑧) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) ∧ 𝑢 ∈ 𝑆) ∧ (𝑢 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))) = 0 ) → (2nd
‘𝑧) ∈ 𝐵) |
| 149 | 5, 7, 146, 129, 148 | ringcld 20257 |
. . . . . . . . . . 11
⊢
(((((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑦 ∼ 𝑧) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) ∧ 𝑢 ∈ 𝑆) ∧ (𝑢 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))) = 0 ) → ((1st
‘𝑥) ·
(2nd ‘𝑧))
∈ 𝐵) |
| 150 | 98, 133 | sseldd 3984 |
. . . . . . . . . . . 12
⊢
(((((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑦 ∼ 𝑧) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) ∧ 𝑢 ∈ 𝑆) ∧ (𝑢 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))) = 0 ) → (2nd
‘𝑥) ∈ 𝐵) |
| 151 | 5, 7, 146, 132, 150 | ringcld 20257 |
. . . . . . . . . . 11
⊢
(((((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑦 ∼ 𝑧) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) ∧ 𝑢 ∈ 𝑆) ∧ (𝑢 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))) = 0 ) → ((1st
‘𝑧) ·
(2nd ‘𝑥))
∈ 𝐵) |
| 152 | 5, 7, 8, 146, 147, 149, 151 | ringsubdi 20304 |
. . . . . . . . . 10
⊢
(((((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑦 ∼ 𝑧) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) ∧ 𝑢 ∈ 𝑆) ∧ (𝑢 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))) = 0 ) → ((2nd
‘𝑦) ·
(((1st ‘𝑥)
·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑥)))) = (((2nd ‘𝑦) · ((1st
‘𝑥) ·
(2nd ‘𝑧)))
−
((2nd ‘𝑦)
·
((1st ‘𝑧)
·
(2nd ‘𝑥))))) |
| 153 | 38 | ad6antr 736 |
. . . . . . . . . . . . 13
⊢
(((((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑦 ∼ 𝑧) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) ∧ 𝑢 ∈ 𝑆) ∧ (𝑢 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))) = 0 ) → 𝑅 ∈ CRing) |
| 154 | 5, 7, 153, 147, 129, 148 | crng12d 20255 |
. . . . . . . . . . . 12
⊢
(((((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑦 ∼ 𝑧) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) ∧ 𝑢 ∈ 𝑆) ∧ (𝑢 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))) = 0 ) → ((2nd
‘𝑦) ·
((1st ‘𝑥)
·
(2nd ‘𝑧)))
= ((1st ‘𝑥) · ((2nd
‘𝑦) ·
(2nd ‘𝑧)))) |
| 155 | 5, 7, 153, 147, 148 | crngcomd 20252 |
. . . . . . . . . . . . 13
⊢
(((((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑦 ∼ 𝑧) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) ∧ 𝑢 ∈ 𝑆) ∧ (𝑢 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))) = 0 ) → ((2nd
‘𝑦) ·
(2nd ‘𝑧))
= ((2nd ‘𝑧) · (2nd
‘𝑦))) |
| 156 | 155 | oveq2d 7447 |
. . . . . . . . . . . 12
⊢
(((((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑦 ∼ 𝑧) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) ∧ 𝑢 ∈ 𝑆) ∧ (𝑢 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))) = 0 ) → ((1st
‘𝑥) ·
((2nd ‘𝑦)
·
(2nd ‘𝑧)))
= ((1st ‘𝑥) · ((2nd
‘𝑧) ·
(2nd ‘𝑦)))) |
| 157 | 5, 7, 153, 129, 148, 147 | crng12d 20255 |
. . . . . . . . . . . 12
⊢
(((((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑦 ∼ 𝑧) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) ∧ 𝑢 ∈ 𝑆) ∧ (𝑢 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))) = 0 ) → ((1st
‘𝑥) ·
((2nd ‘𝑧)
·
(2nd ‘𝑦)))
= ((2nd ‘𝑧) · ((1st
‘𝑥) ·
(2nd ‘𝑦)))) |
| 158 | 154, 156,
157 | 3eqtrd 2781 |
. . . . . . . . . . 11
⊢
(((((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑦 ∼ 𝑧) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) ∧ 𝑢 ∈ 𝑆) ∧ (𝑢 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))) = 0 ) → ((2nd
‘𝑦) ·
((1st ‘𝑥)
·
(2nd ‘𝑧)))
= ((2nd ‘𝑧) · ((1st
‘𝑥) ·
(2nd ‘𝑦)))) |
| 159 | 5, 7, 153, 147, 132, 150 | crng12d 20255 |
. . . . . . . . . . . 12
⊢
(((((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑦 ∼ 𝑧) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) ∧ 𝑢 ∈ 𝑆) ∧ (𝑢 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))) = 0 ) → ((2nd
‘𝑦) ·
((1st ‘𝑧)
·
(2nd ‘𝑥)))
= ((1st ‘𝑧) · ((2nd
‘𝑦) ·
(2nd ‘𝑥)))) |
| 160 | 5, 7, 153, 147, 150 | crngcomd 20252 |
. . . . . . . . . . . . 13
⊢
(((((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑦 ∼ 𝑧) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) ∧ 𝑢 ∈ 𝑆) ∧ (𝑢 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))) = 0 ) → ((2nd
‘𝑦) ·
(2nd ‘𝑥))
= ((2nd ‘𝑥) · (2nd
‘𝑦))) |
| 161 | 160 | oveq2d 7447 |
. . . . . . . . . . . 12
⊢
(((((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑦 ∼ 𝑧) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) ∧ 𝑢 ∈ 𝑆) ∧ (𝑢 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))) = 0 ) → ((1st
‘𝑧) ·
((2nd ‘𝑦)
·
(2nd ‘𝑥)))
= ((1st ‘𝑧) · ((2nd
‘𝑥) ·
(2nd ‘𝑦)))) |
| 162 | 5, 7, 153, 132, 150, 147 | crng12d 20255 |
. . . . . . . . . . . 12
⊢
(((((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑦 ∼ 𝑧) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) ∧ 𝑢 ∈ 𝑆) ∧ (𝑢 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))) = 0 ) → ((1st
‘𝑧) ·
((2nd ‘𝑥)
·
(2nd ‘𝑦)))
= ((2nd ‘𝑥) · ((1st
‘𝑧) ·
(2nd ‘𝑦)))) |
| 163 | 159, 161,
162 | 3eqtrd 2781 |
. . . . . . . . . . 11
⊢
(((((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑦 ∼ 𝑧) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) ∧ 𝑢 ∈ 𝑆) ∧ (𝑢 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))) = 0 ) → ((2nd
‘𝑦) ·
((1st ‘𝑧)
·
(2nd ‘𝑥)))
= ((2nd ‘𝑥) · ((1st
‘𝑧) ·
(2nd ‘𝑦)))) |
| 164 | 158, 163 | oveq12d 7449 |
. . . . . . . . . 10
⊢
(((((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑦 ∼ 𝑧) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) ∧ 𝑢 ∈ 𝑆) ∧ (𝑢 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))) = 0 ) → (((2nd
‘𝑦) ·
((1st ‘𝑥)
·
(2nd ‘𝑧)))
−
((2nd ‘𝑦)
·
((1st ‘𝑧)
·
(2nd ‘𝑥)))) = (((2nd ‘𝑧) · ((1st
‘𝑥) ·
(2nd ‘𝑦)))
−
((2nd ‘𝑥)
·
((1st ‘𝑧)
·
(2nd ‘𝑦))))) |
| 165 | 5, 7, 146, 129, 147 | ringcld 20257 |
. . . . . . . . . . . . 13
⊢
(((((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑦 ∼ 𝑧) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) ∧ 𝑢 ∈ 𝑆) ∧ (𝑢 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))) = 0 ) → ((1st
‘𝑥) ·
(2nd ‘𝑦))
∈ 𝐵) |
| 166 | 142, 55 | syl 17 |
. . . . . . . . . . . . . 14
⊢
(((((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑦 ∼ 𝑧) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) ∧ 𝑢 ∈ 𝑆) ∧ (𝑢 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))) = 0 ) → (1st
‘𝑦) ∈ 𝐵) |
| 167 | 5, 7, 146, 166, 150 | ringcld 20257 |
. . . . . . . . . . . . 13
⊢
(((((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑦 ∼ 𝑧) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) ∧ 𝑢 ∈ 𝑆) ∧ (𝑢 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))) = 0 ) → ((1st
‘𝑦) ·
(2nd ‘𝑥))
∈ 𝐵) |
| 168 | 5, 7, 8, 146, 148, 165, 167 | ringsubdi 20304 |
. . . . . . . . . . . 12
⊢
(((((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑦 ∼ 𝑧) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) ∧ 𝑢 ∈ 𝑆) ∧ (𝑢 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))) = 0 ) → ((2nd
‘𝑧) ·
(((1st ‘𝑥)
·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = (((2nd ‘𝑧) · ((1st
‘𝑥) ·
(2nd ‘𝑦)))
−
((2nd ‘𝑧)
·
((1st ‘𝑦)
·
(2nd ‘𝑥))))) |
| 169 | 5, 7, 146, 166, 148 | ringcld 20257 |
. . . . . . . . . . . . 13
⊢
(((((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑦 ∼ 𝑧) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) ∧ 𝑢 ∈ 𝑆) ∧ (𝑢 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))) = 0 ) → ((1st
‘𝑦) ·
(2nd ‘𝑧))
∈ 𝐵) |
| 170 | 5, 7, 146, 132, 147 | ringcld 20257 |
. . . . . . . . . . . . 13
⊢
(((((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑦 ∼ 𝑧) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) ∧ 𝑢 ∈ 𝑆) ∧ (𝑢 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))) = 0 ) → ((1st
‘𝑧) ·
(2nd ‘𝑦))
∈ 𝐵) |
| 171 | 5, 7, 8, 146, 150, 169, 170 | ringsubdi 20304 |
. . . . . . . . . . . 12
⊢
(((((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑦 ∼ 𝑧) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) ∧ 𝑢 ∈ 𝑆) ∧ (𝑢 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))) = 0 ) → ((2nd
‘𝑥) ·
(((1st ‘𝑦)
·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))) = (((2nd ‘𝑥) · ((1st
‘𝑦) ·
(2nd ‘𝑧)))
−
((2nd ‘𝑥)
·
((1st ‘𝑧)
·
(2nd ‘𝑦))))) |
| 172 | 168, 171 | oveq12d 7449 |
. . . . . . . . . . 11
⊢
(((((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑦 ∼ 𝑧) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) ∧ 𝑢 ∈ 𝑆) ∧ (𝑢 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))) = 0 ) → (((2nd
‘𝑧) ·
(((1st ‘𝑥)
·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥))))(+g‘𝑅)((2nd ‘𝑥) · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦))))) = ((((2nd ‘𝑧) · ((1st
‘𝑥) ·
(2nd ‘𝑦)))
−
((2nd ‘𝑧)
·
((1st ‘𝑦)
·
(2nd ‘𝑥))))(+g‘𝑅)(((2nd ‘𝑥) · ((1st
‘𝑦) ·
(2nd ‘𝑧)))
−
((2nd ‘𝑥)
·
((1st ‘𝑧)
·
(2nd ‘𝑦)))))) |
| 173 | 5, 7, 153, 166, 148, 150 | crng12d 20255 |
. . . . . . . . . . . . 13
⊢
(((((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑦 ∼ 𝑧) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) ∧ 𝑢 ∈ 𝑆) ∧ (𝑢 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))) = 0 ) → ((1st
‘𝑦) ·
((2nd ‘𝑧)
·
(2nd ‘𝑥)))
= ((2nd ‘𝑧) · ((1st
‘𝑦) ·
(2nd ‘𝑥)))) |
| 174 | 173 | oveq2d 7447 |
. . . . . . . . . . . 12
⊢
(((((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑦 ∼ 𝑧) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) ∧ 𝑢 ∈ 𝑆) ∧ (𝑢 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))) = 0 ) → (((2nd
‘𝑧) ·
((1st ‘𝑥)
·
(2nd ‘𝑦)))
−
((1st ‘𝑦)
·
((2nd ‘𝑧)
·
(2nd ‘𝑥)))) = (((2nd ‘𝑧) · ((1st
‘𝑥) ·
(2nd ‘𝑦)))
−
((2nd ‘𝑧)
·
((1st ‘𝑦)
·
(2nd ‘𝑥))))) |
| 175 | 5, 7, 153, 148, 150 | crngcomd 20252 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑦 ∼ 𝑧) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) ∧ 𝑢 ∈ 𝑆) ∧ (𝑢 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))) = 0 ) → ((2nd
‘𝑧) ·
(2nd ‘𝑥))
= ((2nd ‘𝑥) · (2nd
‘𝑧))) |
| 176 | 175 | oveq2d 7447 |
. . . . . . . . . . . . . 14
⊢
(((((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑦 ∼ 𝑧) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) ∧ 𝑢 ∈ 𝑆) ∧ (𝑢 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))) = 0 ) → ((1st
‘𝑦) ·
((2nd ‘𝑧)
·
(2nd ‘𝑥)))
= ((1st ‘𝑦) · ((2nd
‘𝑥) ·
(2nd ‘𝑧)))) |
| 177 | 5, 7, 153, 150, 166, 148 | crng12d 20255 |
. . . . . . . . . . . . . 14
⊢
(((((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑦 ∼ 𝑧) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) ∧ 𝑢 ∈ 𝑆) ∧ (𝑢 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))) = 0 ) → ((2nd
‘𝑥) ·
((1st ‘𝑦)
·
(2nd ‘𝑧)))
= ((1st ‘𝑦) · ((2nd
‘𝑥) ·
(2nd ‘𝑧)))) |
| 178 | 176, 177 | eqtr4d 2780 |
. . . . . . . . . . . . 13
⊢
(((((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑦 ∼ 𝑧) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) ∧ 𝑢 ∈ 𝑆) ∧ (𝑢 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))) = 0 ) → ((1st
‘𝑦) ·
((2nd ‘𝑧)
·
(2nd ‘𝑥)))
= ((2nd ‘𝑥) · ((1st
‘𝑦) ·
(2nd ‘𝑧)))) |
| 179 | 178 | oveq1d 7446 |
. . . . . . . . . . . 12
⊢
(((((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑦 ∼ 𝑧) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) ∧ 𝑢 ∈ 𝑆) ∧ (𝑢 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))) = 0 ) → (((1st
‘𝑦) ·
((2nd ‘𝑧)
·
(2nd ‘𝑥)))
−
((2nd ‘𝑥)
·
((1st ‘𝑧)
·
(2nd ‘𝑦)))) = (((2nd ‘𝑥) · ((1st
‘𝑦) ·
(2nd ‘𝑧)))
−
((2nd ‘𝑥)
·
((1st ‘𝑧)
·
(2nd ‘𝑦))))) |
| 180 | 174, 179 | oveq12d 7449 |
. . . . . . . . . . 11
⊢
(((((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑦 ∼ 𝑧) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) ∧ 𝑢 ∈ 𝑆) ∧ (𝑢 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))) = 0 ) →
((((2nd ‘𝑧) · ((1st
‘𝑥) ·
(2nd ‘𝑦)))
−
((1st ‘𝑦)
·
((2nd ‘𝑧)
·
(2nd ‘𝑥))))(+g‘𝑅)(((1st ‘𝑦) · ((2nd
‘𝑧) ·
(2nd ‘𝑥)))
−
((2nd ‘𝑥)
·
((1st ‘𝑧)
·
(2nd ‘𝑦))))) = ((((2nd ‘𝑧) · ((1st
‘𝑥) ·
(2nd ‘𝑦)))
−
((2nd ‘𝑧)
·
((1st ‘𝑦)
·
(2nd ‘𝑥))))(+g‘𝑅)(((2nd ‘𝑥) · ((1st
‘𝑦) ·
(2nd ‘𝑧)))
−
((2nd ‘𝑥)
·
((1st ‘𝑧)
·
(2nd ‘𝑦)))))) |
| 181 | 40 | ad6antr 736 |
. . . . . . . . . . . 12
⊢
(((((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑦 ∼ 𝑧) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) ∧ 𝑢 ∈ 𝑆) ∧ (𝑢 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))) = 0 ) → 𝑅 ∈ Grp) |
| 182 | 5, 7, 146, 148, 165 | ringcld 20257 |
. . . . . . . . . . . 12
⊢
(((((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑦 ∼ 𝑧) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) ∧ 𝑢 ∈ 𝑆) ∧ (𝑢 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))) = 0 ) → ((2nd
‘𝑧) ·
((1st ‘𝑥)
·
(2nd ‘𝑦)))
∈ 𝐵) |
| 183 | 5, 7, 146, 148, 150 | ringcld 20257 |
. . . . . . . . . . . . 13
⊢
(((((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑦 ∼ 𝑧) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) ∧ 𝑢 ∈ 𝑆) ∧ (𝑢 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))) = 0 ) → ((2nd
‘𝑧) ·
(2nd ‘𝑥))
∈ 𝐵) |
| 184 | 5, 7, 146, 166, 183 | ringcld 20257 |
. . . . . . . . . . . 12
⊢
(((((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑦 ∼ 𝑧) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) ∧ 𝑢 ∈ 𝑆) ∧ (𝑢 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))) = 0 ) → ((1st
‘𝑦) ·
((2nd ‘𝑧)
·
(2nd ‘𝑥)))
∈ 𝐵) |
| 185 | 5, 7, 146, 150, 170 | ringcld 20257 |
. . . . . . . . . . . 12
⊢
(((((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑦 ∼ 𝑧) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) ∧ 𝑢 ∈ 𝑆) ∧ (𝑢 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))) = 0 ) → ((2nd
‘𝑥) ·
((1st ‘𝑧)
·
(2nd ‘𝑦)))
∈ 𝐵) |
| 186 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢
(+g‘𝑅) = (+g‘𝑅) |
| 187 | 5, 186, 8 | grpnpncan 19053 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ Grp ∧
(((2nd ‘𝑧)
·
((1st ‘𝑥)
·
(2nd ‘𝑦)))
∈ 𝐵 ∧
((1st ‘𝑦)
·
((2nd ‘𝑧)
·
(2nd ‘𝑥)))
∈ 𝐵 ∧
((2nd ‘𝑥)
·
((1st ‘𝑧)
·
(2nd ‘𝑦)))
∈ 𝐵)) →
((((2nd ‘𝑧) · ((1st
‘𝑥) ·
(2nd ‘𝑦)))
−
((1st ‘𝑦)
·
((2nd ‘𝑧)
·
(2nd ‘𝑥))))(+g‘𝑅)(((1st ‘𝑦) · ((2nd
‘𝑧) ·
(2nd ‘𝑥)))
−
((2nd ‘𝑥)
·
((1st ‘𝑧)
·
(2nd ‘𝑦))))) = (((2nd ‘𝑧) · ((1st
‘𝑥) ·
(2nd ‘𝑦)))
−
((2nd ‘𝑥)
·
((1st ‘𝑧)
·
(2nd ‘𝑦))))) |
| 188 | 181, 182,
184, 185, 187 | syl13anc 1374 |
. . . . . . . . . . 11
⊢
(((((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑦 ∼ 𝑧) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) ∧ 𝑢 ∈ 𝑆) ∧ (𝑢 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))) = 0 ) →
((((2nd ‘𝑧) · ((1st
‘𝑥) ·
(2nd ‘𝑦)))
−
((1st ‘𝑦)
·
((2nd ‘𝑧)
·
(2nd ‘𝑥))))(+g‘𝑅)(((1st ‘𝑦) · ((2nd
‘𝑧) ·
(2nd ‘𝑥)))
−
((2nd ‘𝑥)
·
((1st ‘𝑧)
·
(2nd ‘𝑦))))) = (((2nd ‘𝑧) · ((1st
‘𝑥) ·
(2nd ‘𝑦)))
−
((2nd ‘𝑥)
·
((1st ‘𝑧)
·
(2nd ‘𝑦))))) |
| 189 | 172, 180,
188 | 3eqtr2rd 2784 |
. . . . . . . . . 10
⊢
(((((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑦 ∼ 𝑧) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) ∧ 𝑢 ∈ 𝑆) ∧ (𝑢 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))) = 0 ) → (((2nd
‘𝑧) ·
((1st ‘𝑥)
·
(2nd ‘𝑦)))
−
((2nd ‘𝑥)
·
((1st ‘𝑧)
·
(2nd ‘𝑦)))) = (((2nd ‘𝑧) · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥))))(+g‘𝑅)((2nd ‘𝑥) · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))))) |
| 190 | 152, 164,
189 | 3eqtrd 2781 |
. . . . . . . . 9
⊢
(((((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑦 ∼ 𝑧) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) ∧ 𝑢 ∈ 𝑆) ∧ (𝑢 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))) = 0 ) → ((2nd
‘𝑦) ·
(((1st ‘𝑥)
·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑥)))) = (((2nd ‘𝑧) · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥))))(+g‘𝑅)((2nd ‘𝑥) · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))))) |
| 191 | 190 | oveq2d 7447 |
. . . . . . . 8
⊢
(((((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑦 ∼ 𝑧) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) ∧ 𝑢 ∈ 𝑆) ∧ (𝑢 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))) = 0 ) → ((𝑡 · 𝑢) · ((2nd
‘𝑦) ·
(((1st ‘𝑥)
·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑥))))) = ((𝑡 · 𝑢) · (((2nd
‘𝑧) ·
(((1st ‘𝑥)
·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥))))(+g‘𝑅)((2nd ‘𝑥) · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦))))))) |
| 192 | 98, 141 | sseldd 3984 |
. . . . . . . . 9
⊢
(((((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑦 ∼ 𝑧) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) ∧ 𝑢 ∈ 𝑆) ∧ (𝑢 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))) = 0 ) → (𝑡 · 𝑢) ∈ 𝐵) |
| 193 | 5, 8 | grpsubcl 19038 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Grp ∧
((1st ‘𝑥)
·
(2nd ‘𝑧))
∈ 𝐵 ∧
((1st ‘𝑧)
·
(2nd ‘𝑥))
∈ 𝐵) →
(((1st ‘𝑥)
·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑥)))
∈ 𝐵) |
| 194 | 181, 149,
151, 193 | syl3anc 1373 |
. . . . . . . . 9
⊢
(((((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑦 ∼ 𝑧) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) ∧ 𝑢 ∈ 𝑆) ∧ (𝑢 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))) = 0 ) → (((1st
‘𝑥) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑥)))
∈ 𝐵) |
| 195 | 5, 7, 146, 192, 147, 194 | ringassd 20254 |
. . . . . . . 8
⊢
(((((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑦 ∼ 𝑧) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) ∧ 𝑢 ∈ 𝑆) ∧ (𝑢 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))) = 0 ) → (((𝑡 · 𝑢) · (2nd
‘𝑦)) ·
(((1st ‘𝑥)
·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑥)))) = ((𝑡 · 𝑢) · ((2nd
‘𝑦) ·
(((1st ‘𝑥)
·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑥)))))) |
| 196 | 98, 138 | sseldd 3984 |
. . . . . . . . . . . . . 14
⊢
(((((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑦 ∼ 𝑧) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) ∧ 𝑢 ∈ 𝑆) ∧ (𝑢 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))) = 0 ) → 𝑢 ∈ 𝐵) |
| 197 | 98, 137 | sseldd 3984 |
. . . . . . . . . . . . . 14
⊢
(((((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑦 ∼ 𝑧) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) ∧ 𝑢 ∈ 𝑆) ∧ (𝑢 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))) = 0 ) → 𝑡 ∈ 𝐵) |
| 198 | 5, 7, 153, 196, 148, 197 | crng32d 20256 |
. . . . . . . . . . . . 13
⊢
(((((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑦 ∼ 𝑧) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) ∧ 𝑢 ∈ 𝑆) ∧ (𝑢 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))) = 0 ) → ((𝑢 · (2nd
‘𝑧)) · 𝑡) = ((𝑢 · 𝑡) · (2nd
‘𝑧))) |
| 199 | 5, 7, 153, 196, 197 | crngcomd 20252 |
. . . . . . . . . . . . . 14
⊢
(((((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑦 ∼ 𝑧) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) ∧ 𝑢 ∈ 𝑆) ∧ (𝑢 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))) = 0 ) → (𝑢 · 𝑡) = (𝑡 · 𝑢)) |
| 200 | 199 | oveq1d 7446 |
. . . . . . . . . . . . 13
⊢
(((((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑦 ∼ 𝑧) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) ∧ 𝑢 ∈ 𝑆) ∧ (𝑢 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))) = 0 ) → ((𝑢 · 𝑡) · (2nd
‘𝑧)) = ((𝑡 · 𝑢) · (2nd
‘𝑧))) |
| 201 | 198, 200 | eqtrd 2777 |
. . . . . . . . . . . 12
⊢
(((((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑦 ∼ 𝑧) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) ∧ 𝑢 ∈ 𝑆) ∧ (𝑢 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))) = 0 ) → ((𝑢 · (2nd
‘𝑧)) · 𝑡) = ((𝑡 · 𝑢) · (2nd
‘𝑧))) |
| 202 | 201 | oveq1d 7446 |
. . . . . . . . . . 11
⊢
(((((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑦 ∼ 𝑧) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) ∧ 𝑢 ∈ 𝑆) ∧ (𝑢 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))) = 0 ) → (((𝑢 · (2nd
‘𝑧)) · 𝑡) · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = (((𝑡 · 𝑢) · (2nd
‘𝑧)) ·
(((1st ‘𝑥)
·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥))))) |
| 203 | 5, 7, 146, 196, 148 | ringcld 20257 |
. . . . . . . . . . . 12
⊢
(((((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑦 ∼ 𝑧) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) ∧ 𝑢 ∈ 𝑆) ∧ (𝑢 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))) = 0 ) → (𝑢 · (2nd
‘𝑧)) ∈ 𝐵) |
| 204 | 181, 165,
167, 68 | syl3anc 1373 |
. . . . . . . . . . . 12
⊢
(((((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑦 ∼ 𝑧) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) ∧ 𝑢 ∈ 𝑆) ∧ (𝑢 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))) = 0 ) → (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))
∈ 𝐵) |
| 205 | 5, 7, 146, 203, 197, 204 | ringassd 20254 |
. . . . . . . . . . 11
⊢
(((((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑦 ∼ 𝑧) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) ∧ 𝑢 ∈ 𝑆) ∧ (𝑢 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))) = 0 ) → (((𝑢 · (2nd
‘𝑧)) · 𝑡) · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = ((𝑢 · (2nd
‘𝑧)) · (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))))) |
| 206 | 5, 7, 146, 192, 148, 204 | ringassd 20254 |
. . . . . . . . . . 11
⊢
(((((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑦 ∼ 𝑧) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) ∧ 𝑢 ∈ 𝑆) ∧ (𝑢 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))) = 0 ) → (((𝑡 · 𝑢) · (2nd
‘𝑧)) ·
(((1st ‘𝑥)
·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = ((𝑡 · 𝑢) · ((2nd
‘𝑧) ·
(((1st ‘𝑥)
·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))))) |
| 207 | 202, 205,
206 | 3eqtr3d 2785 |
. . . . . . . . . 10
⊢
(((((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑦 ∼ 𝑧) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) ∧ 𝑢 ∈ 𝑆) ∧ (𝑢 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))) = 0 ) → ((𝑢 · (2nd
‘𝑧)) · (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥))))) = ((𝑡 · 𝑢) · ((2nd
‘𝑧) ·
(((1st ‘𝑥)
·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))))) |
| 208 | 5, 7, 153, 197, 150, 196 | crng32d 20256 |
. . . . . . . . . . . 12
⊢
(((((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑦 ∼ 𝑧) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) ∧ 𝑢 ∈ 𝑆) ∧ (𝑢 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))) = 0 ) → ((𝑡 · (2nd
‘𝑥)) · 𝑢) = ((𝑡 · 𝑢) · (2nd
‘𝑥))) |
| 209 | 208 | oveq1d 7446 |
. . . . . . . . . . 11
⊢
(((((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑦 ∼ 𝑧) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) ∧ 𝑢 ∈ 𝑆) ∧ (𝑢 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))) = 0 ) → (((𝑡 · (2nd
‘𝑥)) · 𝑢) · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))) = (((𝑡 · 𝑢) · (2nd
‘𝑥)) ·
(((1st ‘𝑦)
·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦))))) |
| 210 | 5, 7, 146, 197, 150 | ringcld 20257 |
. . . . . . . . . . . 12
⊢
(((((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑦 ∼ 𝑧) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) ∧ 𝑢 ∈ 𝑆) ∧ (𝑢 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))) = 0 ) → (𝑡 · (2nd
‘𝑥)) ∈ 𝐵) |
| 211 | 5, 8 | grpsubcl 19038 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ Grp ∧
((1st ‘𝑦)
·
(2nd ‘𝑧))
∈ 𝐵 ∧
((1st ‘𝑧)
·
(2nd ‘𝑦))
∈ 𝐵) →
(((1st ‘𝑦)
·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))
∈ 𝐵) |
| 212 | 181, 169,
170, 211 | syl3anc 1373 |
. . . . . . . . . . . 12
⊢
(((((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑦 ∼ 𝑧) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) ∧ 𝑢 ∈ 𝑆) ∧ (𝑢 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))) = 0 ) → (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))
∈ 𝐵) |
| 213 | 5, 7, 146, 210, 196, 212 | ringassd 20254 |
. . . . . . . . . . 11
⊢
(((((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑦 ∼ 𝑧) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) ∧ 𝑢 ∈ 𝑆) ∧ (𝑢 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))) = 0 ) → (((𝑡 · (2nd
‘𝑥)) · 𝑢) · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))) = ((𝑡 · (2nd
‘𝑥)) · (𝑢 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))))) |
| 214 | 5, 7, 146, 192, 150, 212 | ringassd 20254 |
. . . . . . . . . . 11
⊢
(((((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑦 ∼ 𝑧) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) ∧ 𝑢 ∈ 𝑆) ∧ (𝑢 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))) = 0 ) → (((𝑡 · 𝑢) · (2nd
‘𝑥)) ·
(((1st ‘𝑦)
·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))) = ((𝑡 · 𝑢) · ((2nd
‘𝑥) ·
(((1st ‘𝑦)
·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))))) |
| 215 | 209, 213,
214 | 3eqtr3d 2785 |
. . . . . . . . . 10
⊢
(((((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑦 ∼ 𝑧) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) ∧ 𝑢 ∈ 𝑆) ∧ (𝑢 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))) = 0 ) → ((𝑡 · (2nd
‘𝑥)) · (𝑢 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦))))) = ((𝑡 · 𝑢) · ((2nd
‘𝑥) ·
(((1st ‘𝑦)
·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))))) |
| 216 | 207, 215 | oveq12d 7449 |
. . . . . . . . 9
⊢
(((((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑦 ∼ 𝑧) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) ∧ 𝑢 ∈ 𝑆) ∧ (𝑢 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))) = 0 ) → (((𝑢 · (2nd
‘𝑧)) · (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))))(+g‘𝑅)((𝑡 · (2nd
‘𝑥)) · (𝑢 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))))) = (((𝑡 · 𝑢) · ((2nd
‘𝑧) ·
(((1st ‘𝑥)
·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))))(+g‘𝑅)((𝑡 · 𝑢) · ((2nd
‘𝑥) ·
(((1st ‘𝑦)
·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦))))))) |
| 217 | 5, 7, 146, 148, 204 | ringcld 20257 |
. . . . . . . . . 10
⊢
(((((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑦 ∼ 𝑧) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) ∧ 𝑢 ∈ 𝑆) ∧ (𝑢 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))) = 0 ) → ((2nd
‘𝑧) ·
(((1st ‘𝑥)
·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) ∈ 𝐵) |
| 218 | 5, 7, 146, 150, 212 | ringcld 20257 |
. . . . . . . . . 10
⊢
(((((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑦 ∼ 𝑧) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) ∧ 𝑢 ∈ 𝑆) ∧ (𝑢 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))) = 0 ) → ((2nd
‘𝑥) ·
(((1st ‘𝑦)
·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))) ∈ 𝐵) |
| 219 | 5, 186, 7 | ringdi 20258 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Ring ∧ ((𝑡 · 𝑢) ∈ 𝐵 ∧ ((2nd ‘𝑧) · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) ∈ 𝐵 ∧ ((2nd ‘𝑥) · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))) ∈ 𝐵)) → ((𝑡 · 𝑢) · (((2nd
‘𝑧) ·
(((1st ‘𝑥)
·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥))))(+g‘𝑅)((2nd ‘𝑥) · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))))) = (((𝑡 · 𝑢) · ((2nd
‘𝑧) ·
(((1st ‘𝑥)
·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))))(+g‘𝑅)((𝑡 · 𝑢) · ((2nd
‘𝑥) ·
(((1st ‘𝑦)
·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦))))))) |
| 220 | 146, 192,
217, 218, 219 | syl13anc 1374 |
. . . . . . . . 9
⊢
(((((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑦 ∼ 𝑧) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) ∧ 𝑢 ∈ 𝑆) ∧ (𝑢 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))) = 0 ) → ((𝑡 · 𝑢) · (((2nd
‘𝑧) ·
(((1st ‘𝑥)
·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥))))(+g‘𝑅)((2nd ‘𝑥) · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))))) = (((𝑡 · 𝑢) · ((2nd
‘𝑧) ·
(((1st ‘𝑥)
·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))))(+g‘𝑅)((𝑡 · 𝑢) · ((2nd
‘𝑥) ·
(((1st ‘𝑦)
·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦))))))) |
| 221 | 216, 220 | eqtr4d 2780 |
. . . . . . . 8
⊢
(((((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑦 ∼ 𝑧) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) ∧ 𝑢 ∈ 𝑆) ∧ (𝑢 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))) = 0 ) → (((𝑢 · (2nd
‘𝑧)) · (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))))(+g‘𝑅)((𝑡 · (2nd
‘𝑥)) · (𝑢 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))))) = ((𝑡 · 𝑢) · (((2nd
‘𝑧) ·
(((1st ‘𝑥)
·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥))))(+g‘𝑅)((2nd ‘𝑥) · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦))))))) |
| 222 | 191, 195,
221 | 3eqtr4d 2787 |
. . . . . . 7
⊢
(((((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑦 ∼ 𝑧) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) ∧ 𝑢 ∈ 𝑆) ∧ (𝑢 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))) = 0 ) → (((𝑡 · 𝑢) · (2nd
‘𝑦)) ·
(((1st ‘𝑥)
·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑥)))) = (((𝑢 · (2nd
‘𝑧)) · (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))))(+g‘𝑅)((𝑡 · (2nd
‘𝑥)) · (𝑢 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦))))))) |
| 223 | | simpllr 776 |
. . . . . . . . . 10
⊢
(((((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑦 ∼ 𝑧) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) ∧ 𝑢 ∈ 𝑆) ∧ (𝑢 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))) = 0 ) → (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) |
| 224 | 223 | oveq2d 7447 |
. . . . . . . . 9
⊢
(((((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑦 ∼ 𝑧) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) ∧ 𝑢 ∈ 𝑆) ∧ (𝑢 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))) = 0 ) → ((𝑢 · (2nd
‘𝑧)) · (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥))))) = ((𝑢 · (2nd
‘𝑧)) · 0
)) |
| 225 | 5, 7, 6, 146, 203 | ringrzd 20293 |
. . . . . . . . 9
⊢
(((((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑦 ∼ 𝑧) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) ∧ 𝑢 ∈ 𝑆) ∧ (𝑢 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))) = 0 ) → ((𝑢 · (2nd
‘𝑧)) · 0 ) = 0
) |
| 226 | 224, 225 | eqtrd 2777 |
. . . . . . . 8
⊢
(((((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑦 ∼ 𝑧) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) ∧ 𝑢 ∈ 𝑆) ∧ (𝑢 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))) = 0 ) → ((𝑢 · (2nd
‘𝑧)) · (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥))))) = 0 ) |
| 227 | | simpr 484 |
. . . . . . . . . 10
⊢
(((((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑦 ∼ 𝑧) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) ∧ 𝑢 ∈ 𝑆) ∧ (𝑢 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))) = 0 ) → (𝑢 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))) = 0 ) |
| 228 | 227 | oveq2d 7447 |
. . . . . . . . 9
⊢
(((((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑦 ∼ 𝑧) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) ∧ 𝑢 ∈ 𝑆) ∧ (𝑢 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))) = 0 ) → ((𝑡 · (2nd
‘𝑥)) · (𝑢 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦))))) = ((𝑡 · (2nd
‘𝑥)) · 0
)) |
| 229 | 5, 7, 6, 146, 210 | ringrzd 20293 |
. . . . . . . . 9
⊢
(((((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑦 ∼ 𝑧) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) ∧ 𝑢 ∈ 𝑆) ∧ (𝑢 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))) = 0 ) → ((𝑡 · (2nd
‘𝑥)) · 0 ) = 0
) |
| 230 | 228, 229 | eqtrd 2777 |
. . . . . . . 8
⊢
(((((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑦 ∼ 𝑧) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) ∧ 𝑢 ∈ 𝑆) ∧ (𝑢 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))) = 0 ) → ((𝑡 · (2nd
‘𝑥)) · (𝑢 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦))))) = 0 ) |
| 231 | 226, 230 | oveq12d 7449 |
. . . . . . 7
⊢
(((((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑦 ∼ 𝑧) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) ∧ 𝑢 ∈ 𝑆) ∧ (𝑢 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))) = 0 ) → (((𝑢 · (2nd
‘𝑧)) · (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))))(+g‘𝑅)((𝑡 · (2nd
‘𝑥)) · (𝑢 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))))) = ( 0 (+g‘𝑅) 0 )) |
| 232 | 5, 6 | grpidcl 18983 |
. . . . . . . . 9
⊢ (𝑅 ∈ Grp → 0 ∈ 𝐵) |
| 233 | 181, 232 | syl 17 |
. . . . . . . 8
⊢
(((((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑦 ∼ 𝑧) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) ∧ 𝑢 ∈ 𝑆) ∧ (𝑢 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))) = 0 ) → 0 ∈ 𝐵) |
| 234 | 5, 186, 6, 181, 233 | grplidd 18987 |
. . . . . . 7
⊢
(((((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑦 ∼ 𝑧) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) ∧ 𝑢 ∈ 𝑆) ∧ (𝑢 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))) = 0 ) → ( 0
(+g‘𝑅)
0 ) =
0
) |
| 235 | 222, 231,
234 | 3eqtrd 2781 |
. . . . . 6
⊢
(((((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑦 ∼ 𝑧) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) ∧ 𝑢 ∈ 𝑆) ∧ (𝑢 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))) = 0 ) → (((𝑡 · 𝑢) · (2nd
‘𝑦)) ·
(((1st ‘𝑥)
·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑥)))) = 0 ) |
| 236 | 5, 4, 98, 6, 7, 8,
103, 128, 129, 132, 133, 136, 145, 235 | erlbrd 33267 |
. . . . 5
⊢
(((((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑦 ∼ 𝑧) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) ∧ 𝑢 ∈ 𝑆) ∧ (𝑢 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))) = 0 ) → 𝑥 ∼ 𝑧) |
| 237 | 123 | simprd 495 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑦 ∼ 𝑧) → ∃𝑢 ∈ 𝑆 (𝑢 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))) = 0 ) |
| 238 | 237 | ad2antrr 726 |
. . . . 5
⊢
(((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑦 ∼ 𝑧) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) → ∃𝑢 ∈ 𝑆 (𝑢 · (((1st
‘𝑦) ·
(2nd ‘𝑧))
−
((1st ‘𝑧)
·
(2nd ‘𝑦)))) = 0 ) |
| 239 | 236, 238 | r19.29a 3162 |
. . . 4
⊢
(((((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑦 ∼ 𝑧) ∧ 𝑡 ∈ 𝑆) ∧ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) → 𝑥 ∼ 𝑧) |
| 240 | 37 | adantr 480 |
. . . 4
⊢ (((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑦 ∼ 𝑧) → ∃𝑡 ∈ 𝑆 (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑦))
−
((1st ‘𝑦)
·
(2nd ‘𝑥)))) = 0 ) |
| 241 | 239, 240 | r19.29a 3162 |
. . 3
⊢ (((𝜑 ∧ 𝑥 ∼ 𝑦) ∧ 𝑦 ∼ 𝑧) → 𝑥 ∼ 𝑧) |
| 242 | 241 | anasss 466 |
. 2
⊢ ((𝜑 ∧ (𝑥 ∼ 𝑦 ∧ 𝑦 ∼ 𝑧)) → 𝑥 ∼ 𝑧) |
| 243 | | erler.3 |
. . . . . . . . . . 11
⊢ 1 =
(1r‘𝑅) |
| 244 | 11, 243 | ringidval 20180 |
. . . . . . . . . 10
⊢ 1 =
(0g‘(mulGrp‘𝑅)) |
| 245 | 244 | subm0cl 18824 |
. . . . . . . . 9
⊢ (𝑆 ∈
(SubMnd‘(mulGrp‘𝑅)) → 1 ∈ 𝑆) |
| 246 | 10, 245 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 1 ∈ 𝑆) |
| 247 | 246 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑊) → 1 ∈ 𝑆) |
| 248 | | oveq1 7438 |
. . . . . . . . 9
⊢ (𝑡 = 1 → (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑥))
−
((1st ‘𝑥)
·
(2nd ‘𝑥)))) = ( 1 · (((1st
‘𝑥) ·
(2nd ‘𝑥))
−
((1st ‘𝑥)
·
(2nd ‘𝑥))))) |
| 249 | 248 | eqeq1d 2739 |
. . . . . . . 8
⊢ (𝑡 = 1 → ((𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑥))
−
((1st ‘𝑥)
·
(2nd ‘𝑥)))) = 0 ↔ ( 1 ·
(((1st ‘𝑥)
·
(2nd ‘𝑥))
−
((1st ‘𝑥)
·
(2nd ‘𝑥)))) = 0 )) |
| 250 | 249 | adantl 481 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑊) ∧ 𝑡 = 1 ) → ((𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑥))
−
((1st ‘𝑥)
·
(2nd ‘𝑥)))) = 0 ↔ ( 1 ·
(((1st ‘𝑥)
·
(2nd ‘𝑥))
−
((1st ‘𝑥)
·
(2nd ‘𝑥)))) = 0 )) |
| 251 | 39 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑊) → 𝑅 ∈ Ring) |
| 252 | 45 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑊) → (1st ‘𝑥) ∈ 𝐵) |
| 253 | 14 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑊) → 𝑆 ⊆ 𝐵) |
| 254 | 58 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑊) → (2nd ‘𝑥) ∈ 𝑆) |
| 255 | 253, 254 | sseldd 3984 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑊) → (2nd ‘𝑥) ∈ 𝐵) |
| 256 | 5, 7, 251, 252, 255 | ringcld 20257 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑊) → ((1st ‘𝑥) · (2nd
‘𝑥)) ∈ 𝐵) |
| 257 | 5, 6, 8 | grpsubid 19042 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Grp ∧
((1st ‘𝑥)
·
(2nd ‘𝑥))
∈ 𝐵) →
(((1st ‘𝑥)
·
(2nd ‘𝑥))
−
((1st ‘𝑥)
·
(2nd ‘𝑥)))
= 0
) |
| 258 | 40, 256, 257 | syl2an2r 685 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑊) → (((1st ‘𝑥) · (2nd
‘𝑥)) −
((1st ‘𝑥)
·
(2nd ‘𝑥)))
= 0
) |
| 259 | 258 | oveq2d 7447 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑊) → ( 1 · (((1st
‘𝑥) ·
(2nd ‘𝑥))
−
((1st ‘𝑥)
·
(2nd ‘𝑥)))) = ( 1 · 0 )) |
| 260 | 40, 232 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 0 ∈ 𝐵) |
| 261 | 5, 7, 243, 39, 260 | ringlidmd 20269 |
. . . . . . . . 9
⊢ (𝜑 → ( 1 · 0 ) = 0 ) |
| 262 | 261 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑊) → ( 1 · 0 ) = 0 ) |
| 263 | 259, 262 | eqtrd 2777 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑊) → ( 1 · (((1st
‘𝑥) ·
(2nd ‘𝑥))
−
((1st ‘𝑥)
·
(2nd ‘𝑥)))) = 0 ) |
| 264 | 247, 250,
263 | rspcedvd 3624 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑊) → ∃𝑡 ∈ 𝑆 (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑥))
−
((1st ‘𝑥)
·
(2nd ‘𝑥)))) = 0 ) |
| 265 | 264 | ex 412 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ 𝑊 → ∃𝑡 ∈ 𝑆 (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑥))
−
((1st ‘𝑥)
·
(2nd ‘𝑥)))) = 0 )) |
| 266 | 265 | pm4.71d 561 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ 𝑊 ↔ (𝑥 ∈ 𝑊 ∧ ∃𝑡 ∈ 𝑆 (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑥))
−
((1st ‘𝑥)
·
(2nd ‘𝑥)))) = 0 ))) |
| 267 | | pm4.24 563 |
. . . . 5
⊢ (𝑥 ∈ 𝑊 ↔ (𝑥 ∈ 𝑊 ∧ 𝑥 ∈ 𝑊)) |
| 268 | 267 | anbi1i 624 |
. . . 4
⊢ ((𝑥 ∈ 𝑊 ∧ ∃𝑡 ∈ 𝑆 (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑥))
−
((1st ‘𝑥)
·
(2nd ‘𝑥)))) = 0 ) ↔ ((𝑥 ∈ 𝑊 ∧ 𝑥 ∈ 𝑊) ∧ ∃𝑡 ∈ 𝑆 (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑥))
−
((1st ‘𝑥)
·
(2nd ‘𝑥)))) = 0 )) |
| 269 | 266, 268 | bitrdi 287 |
. . 3
⊢ (𝜑 → (𝑥 ∈ 𝑊 ↔ ((𝑥 ∈ 𝑊 ∧ 𝑥 ∈ 𝑊) ∧ ∃𝑡 ∈ 𝑆 (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑥))
−
((1st ‘𝑥)
·
(2nd ‘𝑥)))) = 0 ))) |
| 270 | | simpl 482 |
. . . . . . . . . . 11
⊢ ((𝑎 = 𝑥 ∧ 𝑏 = 𝑥) → 𝑎 = 𝑥) |
| 271 | 270 | fveq2d 6910 |
. . . . . . . . . 10
⊢ ((𝑎 = 𝑥 ∧ 𝑏 = 𝑥) → (1st ‘𝑎) = (1st ‘𝑥)) |
| 272 | | simpr 484 |
. . . . . . . . . . 11
⊢ ((𝑎 = 𝑥 ∧ 𝑏 = 𝑥) → 𝑏 = 𝑥) |
| 273 | 272 | fveq2d 6910 |
. . . . . . . . . 10
⊢ ((𝑎 = 𝑥 ∧ 𝑏 = 𝑥) → (2nd ‘𝑏) = (2nd ‘𝑥)) |
| 274 | 271, 273 | oveq12d 7449 |
. . . . . . . . 9
⊢ ((𝑎 = 𝑥 ∧ 𝑏 = 𝑥) → ((1st ‘𝑎) · (2nd
‘𝑏)) =
((1st ‘𝑥)
·
(2nd ‘𝑥))) |
| 275 | 272 | fveq2d 6910 |
. . . . . . . . . 10
⊢ ((𝑎 = 𝑥 ∧ 𝑏 = 𝑥) → (1st ‘𝑏) = (1st ‘𝑥)) |
| 276 | 270 | fveq2d 6910 |
. . . . . . . . . 10
⊢ ((𝑎 = 𝑥 ∧ 𝑏 = 𝑥) → (2nd ‘𝑎) = (2nd ‘𝑥)) |
| 277 | 275, 276 | oveq12d 7449 |
. . . . . . . . 9
⊢ ((𝑎 = 𝑥 ∧ 𝑏 = 𝑥) → ((1st ‘𝑏) · (2nd
‘𝑎)) =
((1st ‘𝑥)
·
(2nd ‘𝑥))) |
| 278 | 274, 277 | oveq12d 7449 |
. . . . . . . 8
⊢ ((𝑎 = 𝑥 ∧ 𝑏 = 𝑥) → (((1st ‘𝑎) · (2nd
‘𝑏)) −
((1st ‘𝑏)
·
(2nd ‘𝑎)))
= (((1st ‘𝑥) · (2nd
‘𝑥)) −
((1st ‘𝑥)
·
(2nd ‘𝑥)))) |
| 279 | 278 | oveq2d 7447 |
. . . . . . 7
⊢ ((𝑎 = 𝑥 ∧ 𝑏 = 𝑥) → (𝑡 · (((1st
‘𝑎) ·
(2nd ‘𝑏))
−
((1st ‘𝑏)
·
(2nd ‘𝑎)))) = (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑥))
−
((1st ‘𝑥)
·
(2nd ‘𝑥))))) |
| 280 | 279 | eqeq1d 2739 |
. . . . . 6
⊢ ((𝑎 = 𝑥 ∧ 𝑏 = 𝑥) → ((𝑡 · (((1st
‘𝑎) ·
(2nd ‘𝑏))
−
((1st ‘𝑏)
·
(2nd ‘𝑎)))) = 0 ↔ (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑥))
−
((1st ‘𝑥)
·
(2nd ‘𝑥)))) = 0 )) |
| 281 | 280 | rexbidv 3179 |
. . . . 5
⊢ ((𝑎 = 𝑥 ∧ 𝑏 = 𝑥) → (∃𝑡 ∈ 𝑆 (𝑡 · (((1st
‘𝑎) ·
(2nd ‘𝑏))
−
((1st ‘𝑏)
·
(2nd ‘𝑎)))) = 0 ↔ ∃𝑡 ∈ 𝑆 (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑥))
−
((1st ‘𝑥)
·
(2nd ‘𝑥)))) = 0 )) |
| 282 | 281 | adantl 481 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 = 𝑥 ∧ 𝑏 = 𝑥)) → (∃𝑡 ∈ 𝑆 (𝑡 · (((1st
‘𝑎) ·
(2nd ‘𝑏))
−
((1st ‘𝑏)
·
(2nd ‘𝑎)))) = 0 ↔ ∃𝑡 ∈ 𝑆 (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑥))
−
((1st ‘𝑥)
·
(2nd ‘𝑥)))) = 0 )) |
| 283 | 16, 282 | brab2d 32619 |
. . 3
⊢ (𝜑 → (𝑥 ∼ 𝑥 ↔ ((𝑥 ∈ 𝑊 ∧ 𝑥 ∈ 𝑊) ∧ ∃𝑡 ∈ 𝑆 (𝑡 · (((1st
‘𝑥) ·
(2nd ‘𝑥))
−
((1st ‘𝑥)
·
(2nd ‘𝑥)))) = 0 ))) |
| 284 | 269, 283 | bitr4d 282 |
. 2
⊢ (𝜑 → (𝑥 ∈ 𝑊 ↔ 𝑥 ∼ 𝑥)) |
| 285 | 18, 96, 242, 284 | iserd 8771 |
1
⊢ (𝜑 → ∼ Er 𝑊) |