Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  erler Structured version   Visualization version   GIF version

Theorem erler 33251
Description: The relation used to build the ring localization is an equivalence relation. (Contributed by Thierry Arnoux, 4-May-2025.)
Hypotheses
Ref Expression
erler.1 𝐵 = (Base‘𝑅)
erler.2 0 = (0g𝑅)
erler.3 1 = (1r𝑅)
erler.4 · = (.r𝑅)
erler.5 = (-g𝑅)
erler.w 𝑊 = (𝐵 × 𝑆)
erler.q = (𝑅 ~RL 𝑆)
erler.r (𝜑𝑅 ∈ CRing)
erler.s (𝜑𝑆 ∈ (SubMnd‘(mulGrp‘𝑅)))
Assertion
Ref Expression
erler (𝜑 Er 𝑊)

Proof of Theorem erler
Dummy variables 𝑎 𝑏 𝑡 𝑢 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2734 . . . . 5 {⟨𝑎, 𝑏⟩ ∣ ((𝑎𝑊𝑏𝑊) ∧ ∃𝑡𝑆 (𝑡 · (((1st𝑎) · (2nd𝑏)) ((1st𝑏) · (2nd𝑎)))) = 0 )} = {⟨𝑎, 𝑏⟩ ∣ ((𝑎𝑊𝑏𝑊) ∧ ∃𝑡𝑆 (𝑡 · (((1st𝑎) · (2nd𝑏)) ((1st𝑏) · (2nd𝑎)))) = 0 )}
21relopabiv 5832 . . . 4 Rel {⟨𝑎, 𝑏⟩ ∣ ((𝑎𝑊𝑏𝑊) ∧ ∃𝑡𝑆 (𝑡 · (((1st𝑎) · (2nd𝑏)) ((1st𝑏) · (2nd𝑎)))) = 0 )}
32a1i 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 2734 . . . . . . . . 9 (mulGrp‘𝑅) = (mulGrp‘𝑅)
1211, 5mgpbas 20157 . . . . . . . 8 𝐵 = (Base‘(mulGrp‘𝑅))
1312submss 18834 . . . . . . 7 (𝑆 ∈ (SubMnd‘(mulGrp‘𝑅)) → 𝑆𝐵)
1410, 13syl 17 . . . . . 6 (𝜑𝑆𝐵)
155, 6, 7, 8, 9, 1, 14erlval 33244 . . . . 5 (𝜑 → (𝑅 ~RL 𝑆) = {⟨𝑎, 𝑏⟩ ∣ ((𝑎𝑊𝑏𝑊) ∧ ∃𝑡𝑆 (𝑡 · (((1st𝑎) · (2nd𝑏)) ((1st𝑏) · (2nd𝑎)))) = 0 )})
164, 15eqtrid 2786 . . . 4 (𝜑 = {⟨𝑎, 𝑏⟩ ∣ ((𝑎𝑊𝑏𝑊) ∧ ∃𝑡𝑆 (𝑡 · (((1st𝑎) · (2nd𝑏)) ((1st𝑏) · (2nd𝑎)))) = 0 )})
1716releqd 5790 . . 3 (𝜑 → (Rel ↔ Rel {⟨𝑎, 𝑏⟩ ∣ ((𝑎𝑊𝑏𝑊) ∧ ∃𝑡𝑆 (𝑡 · (((1st𝑎) · (2nd𝑏)) ((1st𝑏) · (2nd𝑎)))) = 0 )}))
183, 17mpbird 257 . 2 (𝜑 → Rel )
19 simpl 482 . . . . . . . . . . . . . . 15 ((𝑎 = 𝑥𝑏 = 𝑦) → 𝑎 = 𝑥)
2019fveq2d 6910 . . . . . . . . . . . . . 14 ((𝑎 = 𝑥𝑏 = 𝑦) → (1st𝑎) = (1st𝑥))
21 simpr 484 . . . . . . . . . . . . . . 15 ((𝑎 = 𝑥𝑏 = 𝑦) → 𝑏 = 𝑦)
2221fveq2d 6910 . . . . . . . . . . . . . 14 ((𝑎 = 𝑥𝑏 = 𝑦) → (2nd𝑏) = (2nd𝑦))
2320, 22oveq12d 7448 . . . . . . . . . . . . 13 ((𝑎 = 𝑥𝑏 = 𝑦) → ((1st𝑎) · (2nd𝑏)) = ((1st𝑥) · (2nd𝑦)))
2421fveq2d 6910 . . . . . . . . . . . . . 14 ((𝑎 = 𝑥𝑏 = 𝑦) → (1st𝑏) = (1st𝑦))
2519fveq2d 6910 . . . . . . . . . . . . . 14 ((𝑎 = 𝑥𝑏 = 𝑦) → (2nd𝑎) = (2nd𝑥))
2624, 25oveq12d 7448 . . . . . . . . . . . . 13 ((𝑎 = 𝑥𝑏 = 𝑦) → ((1st𝑏) · (2nd𝑎)) = ((1st𝑦) · (2nd𝑥)))
2723, 26oveq12d 7448 . . . . . . . . . . . 12 ((𝑎 = 𝑥𝑏 = 𝑦) → (((1st𝑎) · (2nd𝑏)) ((1st𝑏) · (2nd𝑎))) = (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥))))
2827oveq2d 7446 . . . . . . . . . . 11 ((𝑎 = 𝑥𝑏 = 𝑦) → (𝑡 · (((1st𝑎) · (2nd𝑏)) ((1st𝑏) · (2nd𝑎)))) = (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))))
2928eqeq1d 2736 . . . . . . . . . 10 ((𝑎 = 𝑥𝑏 = 𝑦) → ((𝑡 · (((1st𝑎) · (2nd𝑏)) ((1st𝑏) · (2nd𝑎)))) = 0 ↔ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ))
3029rexbidv 3176 . . . . . . . . 9 ((𝑎 = 𝑥𝑏 = 𝑦) → (∃𝑡𝑆 (𝑡 · (((1st𝑎) · (2nd𝑏)) ((1st𝑏) · (2nd𝑎)))) = 0 ↔ ∃𝑡𝑆 (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ))
3130adantl 481 . . . . . . . 8 ((𝜑 ∧ (𝑎 = 𝑥𝑏 = 𝑦)) → (∃𝑡𝑆 (𝑡 · (((1st𝑎) · (2nd𝑏)) ((1st𝑏) · (2nd𝑎)))) = 0 ↔ ∃𝑡𝑆 (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ))
3216, 31brab2d 32626 . . . . . . 7 (𝜑 → (𝑥 𝑦 ↔ ((𝑥𝑊𝑦𝑊) ∧ ∃𝑡𝑆 (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 )))
3332biimpa 476 . . . . . 6 ((𝜑𝑥 𝑦) → ((𝑥𝑊𝑦𝑊) ∧ ∃𝑡𝑆 (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ))
3433simplrd 770 . . . . 5 ((𝜑𝑥 𝑦) → 𝑦𝑊)
3533simplld 768 . . . . 5 ((𝜑𝑥 𝑦) → 𝑥𝑊)
3634, 35jca 511 . . . 4 ((𝜑𝑥 𝑦) → (𝑦𝑊𝑥𝑊))
3733simprd 495 . . . . 5 ((𝜑𝑥 𝑦) → ∃𝑡𝑆 (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 )
38 erler.r . . . . . . . . . . . . 13 (𝜑𝑅 ∈ CRing)
3938crngringd 20263 . . . . . . . . . . . 12 (𝜑𝑅 ∈ Ring)
4039ringgrpd 20259 . . . . . . . . . . 11 (𝜑𝑅 ∈ Grp)
4140ad3antrrr 730 . . . . . . . . . 10 ((((𝜑𝑥 𝑦) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) → 𝑅 ∈ Grp)
4239ad3antrrr 730 . . . . . . . . . . 11 ((((𝜑𝑥 𝑦) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) → 𝑅 ∈ Ring)
4335ad2antrr 726 . . . . . . . . . . . 12 ((((𝜑𝑥 𝑦) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) → 𝑥𝑊)
44 xp1st 8044 . . . . . . . . . . . . 13 (𝑥 ∈ (𝐵 × 𝑆) → (1st𝑥) ∈ 𝐵)
4544, 9eleq2s 2856 . . . . . . . . . . . 12 (𝑥𝑊 → (1st𝑥) ∈ 𝐵)
4643, 45syl 17 . . . . . . . . . . 11 ((((𝜑𝑥 𝑦) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) → (1st𝑥) ∈ 𝐵)
4714ad3antrrr 730 . . . . . . . . . . . 12 ((((𝜑𝑥 𝑦) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) → 𝑆𝐵)
4834ad2antrr 726 . . . . . . . . . . . . 13 ((((𝜑𝑥 𝑦) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) → 𝑦𝑊)
49 xp2nd 8045 . . . . . . . . . . . . . 14 (𝑦 ∈ (𝐵 × 𝑆) → (2nd𝑦) ∈ 𝑆)
5049, 9eleq2s 2856 . . . . . . . . . . . . 13 (𝑦𝑊 → (2nd𝑦) ∈ 𝑆)
5148, 50syl 17 . . . . . . . . . . . 12 ((((𝜑𝑥 𝑦) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) → (2nd𝑦) ∈ 𝑆)
5247, 51sseldd 3995 . . . . . . . . . . 11 ((((𝜑𝑥 𝑦) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) → (2nd𝑦) ∈ 𝐵)
535, 7, 42, 46, 52ringcld 20276 . . . . . . . . . 10 ((((𝜑𝑥 𝑦) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) → ((1st𝑥) · (2nd𝑦)) ∈ 𝐵)
54 xp1st 8044 . . . . . . . . . . . . 13 (𝑦 ∈ (𝐵 × 𝑆) → (1st𝑦) ∈ 𝐵)
5554, 9eleq2s 2856 . . . . . . . . . . . 12 (𝑦𝑊 → (1st𝑦) ∈ 𝐵)
5648, 55syl 17 . . . . . . . . . . 11 ((((𝜑𝑥 𝑦) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) → (1st𝑦) ∈ 𝐵)
57 xp2nd 8045 . . . . . . . . . . . . . 14 (𝑥 ∈ (𝐵 × 𝑆) → (2nd𝑥) ∈ 𝑆)
5857, 9eleq2s 2856 . . . . . . . . . . . . 13 (𝑥𝑊 → (2nd𝑥) ∈ 𝑆)
5943, 58syl 17 . . . . . . . . . . . 12 ((((𝜑𝑥 𝑦) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) → (2nd𝑥) ∈ 𝑆)
6047, 59sseldd 3995 . . . . . . . . . . 11 ((((𝜑𝑥 𝑦) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) → (2nd𝑥) ∈ 𝐵)
615, 7, 42, 56, 60ringcld 20276 . . . . . . . . . 10 ((((𝜑𝑥 𝑦) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) → ((1st𝑦) · (2nd𝑥)) ∈ 𝐵)
62 eqid 2734 . . . . . . . . . . 11 (invg𝑅) = (invg𝑅)
635, 8, 62grpinvsub 19052 . . . . . . . . . 10 ((𝑅 ∈ Grp ∧ ((1st𝑥) · (2nd𝑦)) ∈ 𝐵 ∧ ((1st𝑦) · (2nd𝑥)) ∈ 𝐵) → ((invg𝑅)‘(((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = (((1st𝑦) · (2nd𝑥)) ((1st𝑥) · (2nd𝑦))))
6441, 53, 61, 63syl3anc 1370 . . . . . . . . 9 ((((𝜑𝑥 𝑦) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) → ((invg𝑅)‘(((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = (((1st𝑦) · (2nd𝑥)) ((1st𝑥) · (2nd𝑦))))
6564oveq2d 7446 . . . . . . . 8 ((((𝜑𝑥 𝑦) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) → (𝑡 · ((invg𝑅)‘(((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥))))) = (𝑡 · (((1st𝑦) · (2nd𝑥)) ((1st𝑥) · (2nd𝑦)))))
66 simplr 769 . . . . . . . . . . 11 ((((𝜑𝑥 𝑦) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) → 𝑡𝑆)
6747, 66sseldd 3995 . . . . . . . . . 10 ((((𝜑𝑥 𝑦) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) → 𝑡𝐵)
685, 8grpsubcl 19050 . . . . . . . . . . 11 ((𝑅 ∈ Grp ∧ ((1st𝑥) · (2nd𝑦)) ∈ 𝐵 ∧ ((1st𝑦) · (2nd𝑥)) ∈ 𝐵) → (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥))) ∈ 𝐵)
6941, 53, 61, 68syl3anc 1370 . . . . . . . . . 10 ((((𝜑𝑥 𝑦) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) → (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥))) ∈ 𝐵)
705, 7, 62, 42, 67, 69ringmneg2 20318 . . . . . . . . 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 )
7271fveq2d 6910 . . . . . . . . 9 ((((𝜑𝑥 𝑦) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) → ((invg𝑅)‘(𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥))))) = ((invg𝑅)‘ 0 ))
736, 62grpinvid 19029 . . . . . . . . . 10 (𝑅 ∈ Grp → ((invg𝑅)‘ 0 ) = 0 )
7441, 73syl 17 . . . . . . . . 9 ((((𝜑𝑥 𝑦) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) → ((invg𝑅)‘ 0 ) = 0 )
7570, 72, 743eqtrd 2778 . . . . . . . 8 ((((𝜑𝑥 𝑦) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) → (𝑡 · ((invg𝑅)‘(((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥))))) = 0 )
7665, 75eqtr3d 2776 . . . . . . 7 ((((𝜑𝑥 𝑦) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) → (𝑡 · (((1st𝑦) · (2nd𝑥)) ((1st𝑥) · (2nd𝑦)))) = 0 )
7776ex 412 . . . . . 6 (((𝜑𝑥 𝑦) ∧ 𝑡𝑆) → ((𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 → (𝑡 · (((1st𝑦) · (2nd𝑥)) ((1st𝑥) · (2nd𝑦)))) = 0 ))
7877reximdva 3165 . . . . 5 ((𝜑𝑥 𝑦) → (∃𝑡𝑆 (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 → ∃𝑡𝑆 (𝑡 · (((1st𝑦) · (2nd𝑥)) ((1st𝑥) · (2nd𝑦)))) = 0 ))
7937, 78mpd 15 . . . 4 ((𝜑𝑥 𝑦) → ∃𝑡𝑆 (𝑡 · (((1st𝑦) · (2nd𝑥)) ((1st𝑥) · (2nd𝑦)))) = 0 )
8036, 79jca 511 . . 3 ((𝜑𝑥 𝑦) → ((𝑦𝑊𝑥𝑊) ∧ ∃𝑡𝑆 (𝑡 · (((1st𝑦) · (2nd𝑥)) ((1st𝑥) · (2nd𝑦)))) = 0 ))
81 simpl 482 . . . . . . . . . . . 12 ((𝑎 = 𝑦𝑏 = 𝑥) → 𝑎 = 𝑦)
8281fveq2d 6910 . . . . . . . . . . 11 ((𝑎 = 𝑦𝑏 = 𝑥) → (1st𝑎) = (1st𝑦))
83 simpr 484 . . . . . . . . . . . 12 ((𝑎 = 𝑦𝑏 = 𝑥) → 𝑏 = 𝑥)
8483fveq2d 6910 . . . . . . . . . . 11 ((𝑎 = 𝑦𝑏 = 𝑥) → (2nd𝑏) = (2nd𝑥))
8582, 84oveq12d 7448 . . . . . . . . . 10 ((𝑎 = 𝑦𝑏 = 𝑥) → ((1st𝑎) · (2nd𝑏)) = ((1st𝑦) · (2nd𝑥)))
8683fveq2d 6910 . . . . . . . . . . 11 ((𝑎 = 𝑦𝑏 = 𝑥) → (1st𝑏) = (1st𝑥))
8781fveq2d 6910 . . . . . . . . . . 11 ((𝑎 = 𝑦𝑏 = 𝑥) → (2nd𝑎) = (2nd𝑦))
8886, 87oveq12d 7448 . . . . . . . . . 10 ((𝑎 = 𝑦𝑏 = 𝑥) → ((1st𝑏) · (2nd𝑎)) = ((1st𝑥) · (2nd𝑦)))
8985, 88oveq12d 7448 . . . . . . . . 9 ((𝑎 = 𝑦𝑏 = 𝑥) → (((1st𝑎) · (2nd𝑏)) ((1st𝑏) · (2nd𝑎))) = (((1st𝑦) · (2nd𝑥)) ((1st𝑥) · (2nd𝑦))))
9089oveq2d 7446 . . . . . . . 8 ((𝑎 = 𝑦𝑏 = 𝑥) → (𝑡 · (((1st𝑎) · (2nd𝑏)) ((1st𝑏) · (2nd𝑎)))) = (𝑡 · (((1st𝑦) · (2nd𝑥)) ((1st𝑥) · (2nd𝑦)))))
9190eqeq1d 2736 . . . . . . 7 ((𝑎 = 𝑦𝑏 = 𝑥) → ((𝑡 · (((1st𝑎) · (2nd𝑏)) ((1st𝑏) · (2nd𝑎)))) = 0 ↔ (𝑡 · (((1st𝑦) · (2nd𝑥)) ((1st𝑥) · (2nd𝑦)))) = 0 ))
9291rexbidv 3176 . . . . . 6 ((𝑎 = 𝑦𝑏 = 𝑥) → (∃𝑡𝑆 (𝑡 · (((1st𝑎) · (2nd𝑏)) ((1st𝑏) · (2nd𝑎)))) = 0 ↔ ∃𝑡𝑆 (𝑡 · (((1st𝑦) · (2nd𝑥)) ((1st𝑥) · (2nd𝑦)))) = 0 ))
9392adantl 481 . . . . 5 ((𝜑 ∧ (𝑎 = 𝑦𝑏 = 𝑥)) → (∃𝑡𝑆 (𝑡 · (((1st𝑎) · (2nd𝑏)) ((1st𝑏) · (2nd𝑎)))) = 0 ↔ ∃𝑡𝑆 (𝑡 · (((1st𝑦) · (2nd𝑥)) ((1st𝑥) · (2nd𝑦)))) = 0 ))
9416, 93brab2d 32626 . . . 4 (𝜑 → (𝑦 𝑥 ↔ ((𝑦𝑊𝑥𝑊) ∧ ∃𝑡𝑆 (𝑡 · (((1st𝑦) · (2nd𝑥)) ((1st𝑥) · (2nd𝑦)))) = 0 )))
9594adantr 480 . . 3 ((𝜑𝑥 𝑦) → (𝑦 𝑥 ↔ ((𝑦𝑊𝑥𝑊) ∧ ∃𝑡𝑆 (𝑡 · (((1st𝑦) · (2nd𝑥)) ((1st𝑥) · (2nd𝑦)))) = 0 )))
9680, 95mpbird 257 . 2 ((𝜑𝑥 𝑦) → 𝑦 𝑥)
9710ad6antr 736 . . . . . . 7 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → 𝑆 ∈ (SubMnd‘(mulGrp‘𝑅)))
9897, 13syl 17 . . . . . 6 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → 𝑆𝐵)
9935adantr 480 . . . . . . . . 9 (((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) → 𝑥𝑊)
10099ad4antr 732 . . . . . . . 8 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → 𝑥𝑊)
101100, 9eleqtrdi 2848 . . . . . . 7 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → 𝑥 ∈ (𝐵 × 𝑆))
102 1st2nd2 8051 . . . . . . 7 (𝑥 ∈ (𝐵 × 𝑆) → 𝑥 = ⟨(1st𝑥), (2nd𝑥)⟩)
103101, 102syl 17 . . . . . 6 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → 𝑥 = ⟨(1st𝑥), (2nd𝑥)⟩)
104 simpl 482 . . . . . . . . . . . . . . . . . . . . 21 ((𝑎 = 𝑦𝑏 = 𝑧) → 𝑎 = 𝑦)
105104fveq2d 6910 . . . . . . . . . . . . . . . . . . . 20 ((𝑎 = 𝑦𝑏 = 𝑧) → (1st𝑎) = (1st𝑦))
106 simpr 484 . . . . . . . . . . . . . . . . . . . . 21 ((𝑎 = 𝑦𝑏 = 𝑧) → 𝑏 = 𝑧)
107106fveq2d 6910 . . . . . . . . . . . . . . . . . . . 20 ((𝑎 = 𝑦𝑏 = 𝑧) → (2nd𝑏) = (2nd𝑧))
108105, 107oveq12d 7448 . . . . . . . . . . . . . . . . . . 19 ((𝑎 = 𝑦𝑏 = 𝑧) → ((1st𝑎) · (2nd𝑏)) = ((1st𝑦) · (2nd𝑧)))
109106fveq2d 6910 . . . . . . . . . . . . . . . . . . . 20 ((𝑎 = 𝑦𝑏 = 𝑧) → (1st𝑏) = (1st𝑧))
110104fveq2d 6910 . . . . . . . . . . . . . . . . . . . 20 ((𝑎 = 𝑦𝑏 = 𝑧) → (2nd𝑎) = (2nd𝑦))
111109, 110oveq12d 7448 . . . . . . . . . . . . . . . . . . 19 ((𝑎 = 𝑦𝑏 = 𝑧) → ((1st𝑏) · (2nd𝑎)) = ((1st𝑧) · (2nd𝑦)))
112108, 111oveq12d 7448 . . . . . . . . . . . . . . . . . 18 ((𝑎 = 𝑦𝑏 = 𝑧) → (((1st𝑎) · (2nd𝑏)) ((1st𝑏) · (2nd𝑎))) = (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦))))
113112oveq2d 7446 . . . . . . . . . . . . . . . . 17 ((𝑎 = 𝑦𝑏 = 𝑧) → (𝑡 · (((1st𝑎) · (2nd𝑏)) ((1st𝑏) · (2nd𝑎)))) = (𝑡 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))))
114113eqeq1d 2736 . . . . . . . . . . . . . . . 16 ((𝑎 = 𝑦𝑏 = 𝑧) → ((𝑡 · (((1st𝑎) · (2nd𝑏)) ((1st𝑏) · (2nd𝑎)))) = 0 ↔ (𝑡 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ))
115114rexbidv 3176 . . . . . . . . . . . . . . 15 ((𝑎 = 𝑦𝑏 = 𝑧) → (∃𝑡𝑆 (𝑡 · (((1st𝑎) · (2nd𝑏)) ((1st𝑏) · (2nd𝑎)))) = 0 ↔ ∃𝑡𝑆 (𝑡 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ))
116 oveq1 7437 . . . . . . . . . . . . . . . . 17 (𝑡 = 𝑢 → (𝑡 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))))
117116eqeq1d 2736 . . . . . . . . . . . . . . . 16 (𝑡 = 𝑢 → ((𝑡 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ↔ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ))
118117cbvrexvw 3235 . . . . . . . . . . . . . . 15 (∃𝑡𝑆 (𝑡 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ↔ ∃𝑢𝑆 (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 )
119115, 118bitrdi 287 . . . . . . . . . . . . . 14 ((𝑎 = 𝑦𝑏 = 𝑧) → (∃𝑡𝑆 (𝑡 · (((1st𝑎) · (2nd𝑏)) ((1st𝑏) · (2nd𝑎)))) = 0 ↔ ∃𝑢𝑆 (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ))
120119adantl 481 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑎 = 𝑦𝑏 = 𝑧)) → (∃𝑡𝑆 (𝑡 · (((1st𝑎) · (2nd𝑏)) ((1st𝑏) · (2nd𝑎)))) = 0 ↔ ∃𝑢𝑆 (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ))
12116, 120brab2d 32626 . . . . . . . . . . . 12 (𝜑 → (𝑦 𝑧 ↔ ((𝑦𝑊𝑧𝑊) ∧ ∃𝑢𝑆 (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 )))
122121biimpa 476 . . . . . . . . . . 11 ((𝜑𝑦 𝑧) → ((𝑦𝑊𝑧𝑊) ∧ ∃𝑢𝑆 (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ))
123122adantlr 715 . . . . . . . . . 10 (((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) → ((𝑦𝑊𝑧𝑊) ∧ ∃𝑢𝑆 (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ))
124123simplrd 770 . . . . . . . . 9 (((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) → 𝑧𝑊)
125124ad4antr 732 . . . . . . . 8 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → 𝑧𝑊)
126125, 9eleqtrdi 2848 . . . . . . 7 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → 𝑧 ∈ (𝐵 × 𝑆))
127 1st2nd2 8051 . . . . . . 7 (𝑧 ∈ (𝐵 × 𝑆) → 𝑧 = ⟨(1st𝑧), (2nd𝑧)⟩)
128126, 127syl 17 . . . . . 6 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → 𝑧 = ⟨(1st𝑧), (2nd𝑧)⟩)
129100, 45syl 17 . . . . . 6 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → (1st𝑥) ∈ 𝐵)
130 xp1st 8044 . . . . . . . 8 (𝑧 ∈ (𝐵 × 𝑆) → (1st𝑧) ∈ 𝐵)
131130, 9eleq2s 2856 . . . . . . 7 (𝑧𝑊 → (1st𝑧) ∈ 𝐵)
132125, 131syl 17 . . . . . 6 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → (1st𝑧) ∈ 𝐵)
133100, 58syl 17 . . . . . 6 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → (2nd𝑥) ∈ 𝑆)
134 xp2nd 8045 . . . . . . . 8 (𝑧 ∈ (𝐵 × 𝑆) → (2nd𝑧) ∈ 𝑆)
135134, 9eleq2s 2856 . . . . . . 7 (𝑧𝑊 → (2nd𝑧) ∈ 𝑆)
136125, 135syl 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 ) → 𝑢𝑆)
13911, 7mgpplusg 20155 . . . . . . . . 9 · = (+g‘(mulGrp‘𝑅))
140139submcl 18837 . . . . . . . 8 ((𝑆 ∈ (SubMnd‘(mulGrp‘𝑅)) ∧ 𝑡𝑆𝑢𝑆) → (𝑡 · 𝑢) ∈ 𝑆)
14197, 137, 138, 140syl3anc 1370 . . . . . . 7 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → (𝑡 · 𝑢) ∈ 𝑆)
14234ad5antr 734 . . . . . . . 8 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → 𝑦𝑊)
143142, 50syl 17 . . . . . . 7 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → (2nd𝑦) ∈ 𝑆)
144139submcl 18837 . . . . . . 7 ((𝑆 ∈ (SubMnd‘(mulGrp‘𝑅)) ∧ (𝑡 · 𝑢) ∈ 𝑆 ∧ (2nd𝑦) ∈ 𝑆) → ((𝑡 · 𝑢) · (2nd𝑦)) ∈ 𝑆)
14597, 141, 143, 144syl3anc 1370 . . . . . 6 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → ((𝑡 · 𝑢) · (2nd𝑦)) ∈ 𝑆)
14639ad6antr 736 . . . . . . . . . . 11 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → 𝑅 ∈ Ring)
14798, 143sseldd 3995 . . . . . . . . . . 11 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → (2nd𝑦) ∈ 𝐵)
14898, 136sseldd 3995 . . . . . . . . . . . 12 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → (2nd𝑧) ∈ 𝐵)
1495, 7, 146, 129, 148ringcld 20276 . . . . . . . . . . 11 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → ((1st𝑥) · (2nd𝑧)) ∈ 𝐵)
15098, 133sseldd 3995 . . . . . . . . . . . 12 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → (2nd𝑥) ∈ 𝐵)
1515, 7, 146, 132, 150ringcld 20276 . . . . . . . . . . 11 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → ((1st𝑧) · (2nd𝑥)) ∈ 𝐵)
1525, 7, 8, 146, 147, 149, 151ringsubdi 20320 . . . . . . . . . 10 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → ((2nd𝑦) · (((1st𝑥) · (2nd𝑧)) ((1st𝑧) · (2nd𝑥)))) = (((2nd𝑦) · ((1st𝑥) · (2nd𝑧))) ((2nd𝑦) · ((1st𝑧) · (2nd𝑥)))))
15338ad6antr 736 . . . . . . . . . . . . 13 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → 𝑅 ∈ CRing)
1545, 7, 153, 147, 129, 148crng12d 20275 . . . . . . . . . . . 12 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → ((2nd𝑦) · ((1st𝑥) · (2nd𝑧))) = ((1st𝑥) · ((2nd𝑦) · (2nd𝑧))))
1555, 7, 153, 147, 148crngcomd 20272 . . . . . . . . . . . . 13 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → ((2nd𝑦) · (2nd𝑧)) = ((2nd𝑧) · (2nd𝑦)))
156155oveq2d 7446 . . . . . . . . . . . 12 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → ((1st𝑥) · ((2nd𝑦) · (2nd𝑧))) = ((1st𝑥) · ((2nd𝑧) · (2nd𝑦))))
1575, 7, 153, 129, 148, 147crng12d 20275 . . . . . . . . . . . 12 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → ((1st𝑥) · ((2nd𝑧) · (2nd𝑦))) = ((2nd𝑧) · ((1st𝑥) · (2nd𝑦))))
158154, 156, 1573eqtrd 2778 . . . . . . . . . . 11 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → ((2nd𝑦) · ((1st𝑥) · (2nd𝑧))) = ((2nd𝑧) · ((1st𝑥) · (2nd𝑦))))
1595, 7, 153, 147, 132, 150crng12d 20275 . . . . . . . . . . . 12 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → ((2nd𝑦) · ((1st𝑧) · (2nd𝑥))) = ((1st𝑧) · ((2nd𝑦) · (2nd𝑥))))
1605, 7, 153, 147, 150crngcomd 20272 . . . . . . . . . . . . 13 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → ((2nd𝑦) · (2nd𝑥)) = ((2nd𝑥) · (2nd𝑦)))
161160oveq2d 7446 . . . . . . . . . . . 12 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → ((1st𝑧) · ((2nd𝑦) · (2nd𝑥))) = ((1st𝑧) · ((2nd𝑥) · (2nd𝑦))))
1625, 7, 153, 132, 150, 147crng12d 20275 . . . . . . . . . . . 12 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → ((1st𝑧) · ((2nd𝑥) · (2nd𝑦))) = ((2nd𝑥) · ((1st𝑧) · (2nd𝑦))))
163159, 161, 1623eqtrd 2778 . . . . . . . . . . 11 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → ((2nd𝑦) · ((1st𝑧) · (2nd𝑥))) = ((2nd𝑥) · ((1st𝑧) · (2nd𝑦))))
164158, 163oveq12d 7448 . . . . . . . . . 10 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → (((2nd𝑦) · ((1st𝑥) · (2nd𝑧))) ((2nd𝑦) · ((1st𝑧) · (2nd𝑥)))) = (((2nd𝑧) · ((1st𝑥) · (2nd𝑦))) ((2nd𝑥) · ((1st𝑧) · (2nd𝑦)))))
1655, 7, 146, 129, 147ringcld 20276 . . . . . . . . . . . . 13 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → ((1st𝑥) · (2nd𝑦)) ∈ 𝐵)
166142, 55syl 17 . . . . . . . . . . . . . 14 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → (1st𝑦) ∈ 𝐵)
1675, 7, 146, 166, 150ringcld 20276 . . . . . . . . . . . . 13 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → ((1st𝑦) · (2nd𝑥)) ∈ 𝐵)
1685, 7, 8, 146, 148, 165, 167ringsubdi 20320 . . . . . . . . . . . 12 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → ((2nd𝑧) · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = (((2nd𝑧) · ((1st𝑥) · (2nd𝑦))) ((2nd𝑧) · ((1st𝑦) · (2nd𝑥)))))
1695, 7, 146, 166, 148ringcld 20276 . . . . . . . . . . . . 13 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → ((1st𝑦) · (2nd𝑧)) ∈ 𝐵)
1705, 7, 146, 132, 147ringcld 20276 . . . . . . . . . . . . 13 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → ((1st𝑧) · (2nd𝑦)) ∈ 𝐵)
1715, 7, 8, 146, 150, 169, 170ringsubdi 20320 . . . . . . . . . . . 12 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → ((2nd𝑥) · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = (((2nd𝑥) · ((1st𝑦) · (2nd𝑧))) ((2nd𝑥) · ((1st𝑧) · (2nd𝑦)))))
172168, 171oveq12d 7448 . . . . . . . . . . 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𝑦))))))
1735, 7, 153, 166, 148, 150crng12d 20275 . . . . . . . . . . . . 13 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → ((1st𝑦) · ((2nd𝑧) · (2nd𝑥))) = ((2nd𝑧) · ((1st𝑦) · (2nd𝑥))))
174173oveq2d 7446 . . . . . . . . . . . 12 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → (((2nd𝑧) · ((1st𝑥) · (2nd𝑦))) ((1st𝑦) · ((2nd𝑧) · (2nd𝑥)))) = (((2nd𝑧) · ((1st𝑥) · (2nd𝑦))) ((2nd𝑧) · ((1st𝑦) · (2nd𝑥)))))
1755, 7, 153, 148, 150crngcomd 20272 . . . . . . . . . . . . . . 15 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → ((2nd𝑧) · (2nd𝑥)) = ((2nd𝑥) · (2nd𝑧)))
176175oveq2d 7446 . . . . . . . . . . . . . 14 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → ((1st𝑦) · ((2nd𝑧) · (2nd𝑥))) = ((1st𝑦) · ((2nd𝑥) · (2nd𝑧))))
1775, 7, 153, 150, 166, 148crng12d 20275 . . . . . . . . . . . . . 14 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → ((2nd𝑥) · ((1st𝑦) · (2nd𝑧))) = ((1st𝑦) · ((2nd𝑥) · (2nd𝑧))))
178176, 177eqtr4d 2777 . . . . . . . . . . . . 13 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → ((1st𝑦) · ((2nd𝑧) · (2nd𝑥))) = ((2nd𝑥) · ((1st𝑦) · (2nd𝑧))))
179178oveq1d 7445 . . . . . . . . . . . 12 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → (((1st𝑦) · ((2nd𝑧) · (2nd𝑥))) ((2nd𝑥) · ((1st𝑧) · (2nd𝑦)))) = (((2nd𝑥) · ((1st𝑦) · (2nd𝑧))) ((2nd𝑥) · ((1st𝑧) · (2nd𝑦)))))
180174, 179oveq12d 7448 . . . . . . . . . . 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𝑦))))))
18140ad6antr 736 . . . . . . . . . . . 12 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → 𝑅 ∈ Grp)
1825, 7, 146, 148, 165ringcld 20276 . . . . . . . . . . . 12 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → ((2nd𝑧) · ((1st𝑥) · (2nd𝑦))) ∈ 𝐵)
1835, 7, 146, 148, 150ringcld 20276 . . . . . . . . . . . . 13 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → ((2nd𝑧) · (2nd𝑥)) ∈ 𝐵)
1845, 7, 146, 166, 183ringcld 20276 . . . . . . . . . . . 12 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → ((1st𝑦) · ((2nd𝑧) · (2nd𝑥))) ∈ 𝐵)
1855, 7, 146, 150, 170ringcld 20276 . . . . . . . . . . . 12 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → ((2nd𝑥) · ((1st𝑧) · (2nd𝑦))) ∈ 𝐵)
186 eqid 2734 . . . . . . . . . . . . 13 (+g𝑅) = (+g𝑅)
1875, 186, 8grpnpncan 19065 . . . . . . . . . . . 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𝑦)))))
188181, 182, 184, 185, 187syl13anc 1371 . . . . . . . . . . 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𝑦)))))
189172, 180, 1883eqtr2rd 2781 . . . . . . . . . 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𝑦))))))
190152, 164, 1893eqtrd 2778 . . . . . . . . 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𝑦))))))
191190oveq2d 7446 . . . . . . . 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𝑦)))))))
19298, 141sseldd 3995 . . . . . . . . 9 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → (𝑡 · 𝑢) ∈ 𝐵)
1935, 8grpsubcl 19050 . . . . . . . . . 10 ((𝑅 ∈ Grp ∧ ((1st𝑥) · (2nd𝑧)) ∈ 𝐵 ∧ ((1st𝑧) · (2nd𝑥)) ∈ 𝐵) → (((1st𝑥) · (2nd𝑧)) ((1st𝑧) · (2nd𝑥))) ∈ 𝐵)
194181, 149, 151, 193syl3anc 1370 . . . . . . . . 9 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → (((1st𝑥) · (2nd𝑧)) ((1st𝑧) · (2nd𝑥))) ∈ 𝐵)
1955, 7, 146, 192, 147, 194ringassd 20274 . . . . . . . 8 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → (((𝑡 · 𝑢) · (2nd𝑦)) · (((1st𝑥) · (2nd𝑧)) ((1st𝑧) · (2nd𝑥)))) = ((𝑡 · 𝑢) · ((2nd𝑦) · (((1st𝑥) · (2nd𝑧)) ((1st𝑧) · (2nd𝑥))))))
19698, 138sseldd 3995 . . . . . . . . . . . . . 14 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → 𝑢𝐵)
19798, 137sseldd 3995 . . . . . . . . . . . . . 14 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → 𝑡𝐵)
1985, 7, 153, 196, 148, 197cringmul32d 33217 . . . . . . . . . . . . 13 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → ((𝑢 · (2nd𝑧)) · 𝑡) = ((𝑢 · 𝑡) · (2nd𝑧)))
1995, 7, 153, 196, 197crngcomd 20272 . . . . . . . . . . . . . 14 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → (𝑢 · 𝑡) = (𝑡 · 𝑢))
200199oveq1d 7445 . . . . . . . . . . . . 13 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → ((𝑢 · 𝑡) · (2nd𝑧)) = ((𝑡 · 𝑢) · (2nd𝑧)))
201198, 200eqtrd 2774 . . . . . . . . . . . 12 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → ((𝑢 · (2nd𝑧)) · 𝑡) = ((𝑡 · 𝑢) · (2nd𝑧)))
202201oveq1d 7445 . . . . . . . . . . 11 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → (((𝑢 · (2nd𝑧)) · 𝑡) · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = (((𝑡 · 𝑢) · (2nd𝑧)) · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))))
2035, 7, 146, 196, 148ringcld 20276 . . . . . . . . . . . 12 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → (𝑢 · (2nd𝑧)) ∈ 𝐵)
204181, 165, 167, 68syl3anc 1370 . . . . . . . . . . . 12 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥))) ∈ 𝐵)
2055, 7, 146, 203, 197, 204ringassd 20274 . . . . . . . . . . 11 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → (((𝑢 · (2nd𝑧)) · 𝑡) · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = ((𝑢 · (2nd𝑧)) · (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥))))))
2065, 7, 146, 192, 148, 204ringassd 20274 . . . . . . . . . . 11 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → (((𝑡 · 𝑢) · (2nd𝑧)) · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = ((𝑡 · 𝑢) · ((2nd𝑧) · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥))))))
207202, 205, 2063eqtr3d 2782 . . . . . . . . . 10 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → ((𝑢 · (2nd𝑧)) · (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥))))) = ((𝑡 · 𝑢) · ((2nd𝑧) · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥))))))
2085, 7, 153, 197, 150, 196cringmul32d 33217 . . . . . . . . . . . 12 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → ((𝑡 · (2nd𝑥)) · 𝑢) = ((𝑡 · 𝑢) · (2nd𝑥)))
209208oveq1d 7445 . . . . . . . . . . 11 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → (((𝑡 · (2nd𝑥)) · 𝑢) · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = (((𝑡 · 𝑢) · (2nd𝑥)) · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))))
2105, 7, 146, 197, 150ringcld 20276 . . . . . . . . . . . 12 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → (𝑡 · (2nd𝑥)) ∈ 𝐵)
2115, 8grpsubcl 19050 . . . . . . . . . . . . 13 ((𝑅 ∈ Grp ∧ ((1st𝑦) · (2nd𝑧)) ∈ 𝐵 ∧ ((1st𝑧) · (2nd𝑦)) ∈ 𝐵) → (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦))) ∈ 𝐵)
212181, 169, 170, 211syl3anc 1370 . . . . . . . . . . . 12 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦))) ∈ 𝐵)
2135, 7, 146, 210, 196, 212ringassd 20274 . . . . . . . . . . 11 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → (((𝑡 · (2nd𝑥)) · 𝑢) · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = ((𝑡 · (2nd𝑥)) · (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦))))))
2145, 7, 146, 192, 150, 212ringassd 20274 . . . . . . . . . . 11 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → (((𝑡 · 𝑢) · (2nd𝑥)) · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = ((𝑡 · 𝑢) · ((2nd𝑥) · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦))))))
215209, 213, 2143eqtr3d 2782 . . . . . . . . . 10 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → ((𝑡 · (2nd𝑥)) · (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦))))) = ((𝑡 · 𝑢) · ((2nd𝑥) · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦))))))
216207, 215oveq12d 7448 . . . . . . . . 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𝑦)))))))
2175, 7, 146, 148, 204ringcld 20276 . . . . . . . . . 10 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → ((2nd𝑧) · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) ∈ 𝐵)
2185, 7, 146, 150, 212ringcld 20276 . . . . . . . . . 10 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → ((2nd𝑥) · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) ∈ 𝐵)
2195, 186, 7ringdi 20277 . . . . . . . . . 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𝑦)))))))
220146, 192, 217, 218, 219syl13anc 1371 . . . . . . . . 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𝑦)))))))
221216, 220eqtr4d 2777 . . . . . . . 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𝑦)))))))
222191, 195, 2213eqtr4d 2784 . . . . . . 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 )
224223oveq2d 7446 . . . . . . . . 9 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → ((𝑢 · (2nd𝑧)) · (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥))))) = ((𝑢 · (2nd𝑧)) · 0 ))
2255, 7, 6, 146, 203ringrzd 20309 . . . . . . . . 9 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → ((𝑢 · (2nd𝑧)) · 0 ) = 0 )
226224, 225eqtrd 2774 . . . . . . . 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 )
228227oveq2d 7446 . . . . . . . . 9 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → ((𝑡 · (2nd𝑥)) · (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦))))) = ((𝑡 · (2nd𝑥)) · 0 ))
2295, 7, 6, 146, 210ringrzd 20309 . . . . . . . . 9 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → ((𝑡 · (2nd𝑥)) · 0 ) = 0 )
230228, 229eqtrd 2774 . . . . . . . 8 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → ((𝑡 · (2nd𝑥)) · (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦))))) = 0 )
231226, 230oveq12d 7448 . . . . . . 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 ))
2325, 6grpidcl 18995 . . . . . . . . 9 (𝑅 ∈ Grp → 0𝐵)
233181, 232syl 17 . . . . . . . 8 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → 0𝐵)
2345, 186, 6, 181, 233grplidd 18999 . . . . . . 7 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → ( 0 (+g𝑅) 0 ) = 0 )
235222, 231, 2343eqtrd 2778 . . . . . 6 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → (((𝑡 · 𝑢) · (2nd𝑦)) · (((1st𝑥) · (2nd𝑧)) ((1st𝑧) · (2nd𝑥)))) = 0 )
2365, 4, 98, 6, 7, 8, 103, 128, 129, 132, 133, 136, 145, 235erlbrd 33249 . . . . 5 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → 𝑥 𝑧)
237123simprd 495 . . . . . 6 (((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) → ∃𝑢𝑆 (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 )
238237ad2antrr 726 . . . . 5 (((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) → ∃𝑢𝑆 (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 )
239236, 238r19.29a 3159 . . . 4 (((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) → 𝑥 𝑧)
24037adantr 480 . . . 4 (((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) → ∃𝑡𝑆 (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 )
241239, 240r19.29a 3159 . . 3 (((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) → 𝑥 𝑧)
242241anasss 466 . 2 ((𝜑 ∧ (𝑥 𝑦𝑦 𝑧)) → 𝑥 𝑧)
243 erler.3 . . . . . . . . . . 11 1 = (1r𝑅)
24411, 243ringidval 20200 . . . . . . . . . 10 1 = (0g‘(mulGrp‘𝑅))
245244subm0cl 18836 . . . . . . . . 9 (𝑆 ∈ (SubMnd‘(mulGrp‘𝑅)) → 1𝑆)
24610, 245syl 17 . . . . . . . 8 (𝜑1𝑆)
247246adantr 480 . . . . . . 7 ((𝜑𝑥𝑊) → 1𝑆)
248 oveq1 7437 . . . . . . . . 9 (𝑡 = 1 → (𝑡 · (((1st𝑥) · (2nd𝑥)) ((1st𝑥) · (2nd𝑥)))) = ( 1 · (((1st𝑥) · (2nd𝑥)) ((1st𝑥) · (2nd𝑥)))))
249248eqeq1d 2736 . . . . . . . 8 (𝑡 = 1 → ((𝑡 · (((1st𝑥) · (2nd𝑥)) ((1st𝑥) · (2nd𝑥)))) = 0 ↔ ( 1 · (((1st𝑥) · (2nd𝑥)) ((1st𝑥) · (2nd𝑥)))) = 0 ))
250249adantl 481 . . . . . . 7 (((𝜑𝑥𝑊) ∧ 𝑡 = 1 ) → ((𝑡 · (((1st𝑥) · (2nd𝑥)) ((1st𝑥) · (2nd𝑥)))) = 0 ↔ ( 1 · (((1st𝑥) · (2nd𝑥)) ((1st𝑥) · (2nd𝑥)))) = 0 ))
25139adantr 480 . . . . . . . . . . 11 ((𝜑𝑥𝑊) → 𝑅 ∈ Ring)
25245adantl 481 . . . . . . . . . . 11 ((𝜑𝑥𝑊) → (1st𝑥) ∈ 𝐵)
25314adantr 480 . . . . . . . . . . . 12 ((𝜑𝑥𝑊) → 𝑆𝐵)
25458adantl 481 . . . . . . . . . . . 12 ((𝜑𝑥𝑊) → (2nd𝑥) ∈ 𝑆)
255253, 254sseldd 3995 . . . . . . . . . . 11 ((𝜑𝑥𝑊) → (2nd𝑥) ∈ 𝐵)
2565, 7, 251, 252, 255ringcld 20276 . . . . . . . . . 10 ((𝜑𝑥𝑊) → ((1st𝑥) · (2nd𝑥)) ∈ 𝐵)
2575, 6, 8grpsubid 19054 . . . . . . . . . 10 ((𝑅 ∈ Grp ∧ ((1st𝑥) · (2nd𝑥)) ∈ 𝐵) → (((1st𝑥) · (2nd𝑥)) ((1st𝑥) · (2nd𝑥))) = 0 )
25840, 256, 257syl2an2r 685 . . . . . . . . 9 ((𝜑𝑥𝑊) → (((1st𝑥) · (2nd𝑥)) ((1st𝑥) · (2nd𝑥))) = 0 )
259258oveq2d 7446 . . . . . . . 8 ((𝜑𝑥𝑊) → ( 1 · (((1st𝑥) · (2nd𝑥)) ((1st𝑥) · (2nd𝑥)))) = ( 1 · 0 ))
26040, 232syl 17 . . . . . . . . . 10 (𝜑0𝐵)
2615, 7, 243, 39, 260ringlidmd 20285 . . . . . . . . 9 (𝜑 → ( 1 · 0 ) = 0 )
262261adantr 480 . . . . . . . 8 ((𝜑𝑥𝑊) → ( 1 · 0 ) = 0 )
263259, 262eqtrd 2774 . . . . . . 7 ((𝜑𝑥𝑊) → ( 1 · (((1st𝑥) · (2nd𝑥)) ((1st𝑥) · (2nd𝑥)))) = 0 )
264247, 250, 263rspcedvd 3623 . . . . . 6 ((𝜑𝑥𝑊) → ∃𝑡𝑆 (𝑡 · (((1st𝑥) · (2nd𝑥)) ((1st𝑥) · (2nd𝑥)))) = 0 )
265264ex 412 . . . . 5 (𝜑 → (𝑥𝑊 → ∃𝑡𝑆 (𝑡 · (((1st𝑥) · (2nd𝑥)) ((1st𝑥) · (2nd𝑥)))) = 0 ))
266265pm4.71d 561 . . . 4 (𝜑 → (𝑥𝑊 ↔ (𝑥𝑊 ∧ ∃𝑡𝑆 (𝑡 · (((1st𝑥) · (2nd𝑥)) ((1st𝑥) · (2nd𝑥)))) = 0 )))
267 pm4.24 563 . . . . 5 (𝑥𝑊 ↔ (𝑥𝑊𝑥𝑊))
268267anbi1i 624 . . . 4 ((𝑥𝑊 ∧ ∃𝑡𝑆 (𝑡 · (((1st𝑥) · (2nd𝑥)) ((1st𝑥) · (2nd𝑥)))) = 0 ) ↔ ((𝑥𝑊𝑥𝑊) ∧ ∃𝑡𝑆 (𝑡 · (((1st𝑥) · (2nd𝑥)) ((1st𝑥) · (2nd𝑥)))) = 0 ))
269266, 268bitrdi 287 . . 3 (𝜑 → (𝑥𝑊 ↔ ((𝑥𝑊𝑥𝑊) ∧ ∃𝑡𝑆 (𝑡 · (((1st𝑥) · (2nd𝑥)) ((1st𝑥) · (2nd𝑥)))) = 0 )))
270 simpl 482 . . . . . . . . . . 11 ((𝑎 = 𝑥𝑏 = 𝑥) → 𝑎 = 𝑥)
271270fveq2d 6910 . . . . . . . . . 10 ((𝑎 = 𝑥𝑏 = 𝑥) → (1st𝑎) = (1st𝑥))
272 simpr 484 . . . . . . . . . . 11 ((𝑎 = 𝑥𝑏 = 𝑥) → 𝑏 = 𝑥)
273272fveq2d 6910 . . . . . . . . . 10 ((𝑎 = 𝑥𝑏 = 𝑥) → (2nd𝑏) = (2nd𝑥))
274271, 273oveq12d 7448 . . . . . . . . 9 ((𝑎 = 𝑥𝑏 = 𝑥) → ((1st𝑎) · (2nd𝑏)) = ((1st𝑥) · (2nd𝑥)))
275272fveq2d 6910 . . . . . . . . . 10 ((𝑎 = 𝑥𝑏 = 𝑥) → (1st𝑏) = (1st𝑥))
276270fveq2d 6910 . . . . . . . . . 10 ((𝑎 = 𝑥𝑏 = 𝑥) → (2nd𝑎) = (2nd𝑥))
277275, 276oveq12d 7448 . . . . . . . . 9 ((𝑎 = 𝑥𝑏 = 𝑥) → ((1st𝑏) · (2nd𝑎)) = ((1st𝑥) · (2nd𝑥)))
278274, 277oveq12d 7448 . . . . . . . 8 ((𝑎 = 𝑥𝑏 = 𝑥) → (((1st𝑎) · (2nd𝑏)) ((1st𝑏) · (2nd𝑎))) = (((1st𝑥) · (2nd𝑥)) ((1st𝑥) · (2nd𝑥))))
279278oveq2d 7446 . . . . . . 7 ((𝑎 = 𝑥𝑏 = 𝑥) → (𝑡 · (((1st𝑎) · (2nd𝑏)) ((1st𝑏) · (2nd𝑎)))) = (𝑡 · (((1st𝑥) · (2nd𝑥)) ((1st𝑥) · (2nd𝑥)))))
280279eqeq1d 2736 . . . . . 6 ((𝑎 = 𝑥𝑏 = 𝑥) → ((𝑡 · (((1st𝑎) · (2nd𝑏)) ((1st𝑏) · (2nd𝑎)))) = 0 ↔ (𝑡 · (((1st𝑥) · (2nd𝑥)) ((1st𝑥) · (2nd𝑥)))) = 0 ))
281280rexbidv 3176 . . . . 5 ((𝑎 = 𝑥𝑏 = 𝑥) → (∃𝑡𝑆 (𝑡 · (((1st𝑎) · (2nd𝑏)) ((1st𝑏) · (2nd𝑎)))) = 0 ↔ ∃𝑡𝑆 (𝑡 · (((1st𝑥) · (2nd𝑥)) ((1st𝑥) · (2nd𝑥)))) = 0 ))
282281adantl 481 . . . 4 ((𝜑 ∧ (𝑎 = 𝑥𝑏 = 𝑥)) → (∃𝑡𝑆 (𝑡 · (((1st𝑎) · (2nd𝑏)) ((1st𝑏) · (2nd𝑎)))) = 0 ↔ ∃𝑡𝑆 (𝑡 · (((1st𝑥) · (2nd𝑥)) ((1st𝑥) · (2nd𝑥)))) = 0 ))
28316, 282brab2d 32626 . . 3 (𝜑 → (𝑥 𝑥 ↔ ((𝑥𝑊𝑥𝑊) ∧ ∃𝑡𝑆 (𝑡 · (((1st𝑥) · (2nd𝑥)) ((1st𝑥) · (2nd𝑥)))) = 0 )))
284269, 283bitr4d 282 . 2 (𝜑 → (𝑥𝑊𝑥 𝑥))
28518, 96, 242, 284iserd 8769 1 (𝜑 Er 𝑊)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395   = wceq 1536  wcel 2105  wrex 3067  wss 3962  cop 4636   class class class wbr 5147  {copab 5209   × cxp 5686  Rel wrel 5693  cfv 6562  (class class class)co 7430  1st c1st 8010  2nd c2nd 8011   Er wer 8740  Basecbs 17244  +gcplusg 17297  .rcmulr 17298  0gc0g 17485  SubMndcsubmnd 18807  Grpcgrp 18963  invgcminusg 18964  -gcsg 18965  mulGrpcmgp 20151  1rcur 20198  Ringcrg 20250  CRingccrg 20251   ~RL cerl 33239
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753  ax-cnex 11208  ax-resscn 11209  ax-1cn 11210  ax-icn 11211  ax-addcl 11212  ax-addrcl 11213  ax-mulcl 11214  ax-mulrcl 11215  ax-mulcom 11216  ax-addass 11217  ax-mulass 11218  ax-distr 11219  ax-i2m1 11220  ax-1ne0 11221  ax-1rid 11222  ax-rnegex 11223  ax-rrecex 11224  ax-cnre 11225  ax-pre-lttri 11226  ax-pre-lttrn 11227  ax-pre-ltadd 11228  ax-pre-mulgt0 11229
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-rmo 3377  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-iun 4997  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-we 5642  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-pred 6322  df-ord 6388  df-on 6389  df-lim 6390  df-suc 6391  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-riota 7387  df-ov 7433  df-oprab 7434  df-mpo 7435  df-om 7887  df-1st 8012  df-2nd 8013  df-frecs 8304  df-wrecs 8335  df-recs 8409  df-rdg 8448  df-er 8743  df-en 8984  df-dom 8985  df-sdom 8986  df-pnf 11294  df-mnf 11295  df-xr 11296  df-ltxr 11297  df-le 11298  df-sub 11491  df-neg 11492  df-nn 12264  df-2 12326  df-sets 17197  df-slot 17215  df-ndx 17227  df-base 17245  df-ress 17274  df-plusg 17310  df-0g 17487  df-mgm 18665  df-sgrp 18744  df-mnd 18760  df-submnd 18809  df-grp 18966  df-minusg 18967  df-sbg 18968  df-cmn 19814  df-abl 19815  df-mgp 20152  df-rng 20170  df-ur 20199  df-ring 20252  df-cring 20253  df-erl 33241
This theorem is referenced by:  rlocaddval  33254  rlocmulval  33255  rloccring  33256  rlocf1  33259  fracfld  33289  zringfrac  33561
  Copyright terms: Public domain W3C validator