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 33269
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 2737 . . . . 5 {⟨𝑎, 𝑏⟩ ∣ ((𝑎𝑊𝑏𝑊) ∧ ∃𝑡𝑆 (𝑡 · (((1st𝑎) · (2nd𝑏)) ((1st𝑏) · (2nd𝑎)))) = 0 )} = {⟨𝑎, 𝑏⟩ ∣ ((𝑎𝑊𝑏𝑊) ∧ ∃𝑡𝑆 (𝑡 · (((1st𝑎) · (2nd𝑏)) ((1st𝑏) · (2nd𝑎)))) = 0 )}
21relopabiv 5830 . . . 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 2737 . . . . . . . . 9 (mulGrp‘𝑅) = (mulGrp‘𝑅)
1211, 5mgpbas 20142 . . . . . . . 8 𝐵 = (Base‘(mulGrp‘𝑅))
1312submss 18822 . . . . . . 7 (𝑆 ∈ (SubMnd‘(mulGrp‘𝑅)) → 𝑆𝐵)
1410, 13syl 17 . . . . . 6 (𝜑𝑆𝐵)
155, 6, 7, 8, 9, 1, 14erlval 33262 . . . . 5 (𝜑 → (𝑅 ~RL 𝑆) = {⟨𝑎, 𝑏⟩ ∣ ((𝑎𝑊𝑏𝑊) ∧ ∃𝑡𝑆 (𝑡 · (((1st𝑎) · (2nd𝑏)) ((1st𝑏) · (2nd𝑎)))) = 0 )})
164, 15eqtrid 2789 . . . 4 (𝜑 = {⟨𝑎, 𝑏⟩ ∣ ((𝑎𝑊𝑏𝑊) ∧ ∃𝑡𝑆 (𝑡 · (((1st𝑎) · (2nd𝑏)) ((1st𝑏) · (2nd𝑎)))) = 0 )})
1716releqd 5788 . . 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 7449 . . . . . . . . . . . . 13 ((𝑎 = 𝑥𝑏 = 𝑦) → ((1st𝑎) · (2nd𝑏)) = ((1st𝑥) · (2nd𝑦)))
2421fveq2d 6910 . . . . . . . . . . . . . 14 ((𝑎 = 𝑥𝑏 = 𝑦) → (1st𝑏) = (1st𝑦))
2519fveq2d 6910 . . . . . . . . . . . . . 14 ((𝑎 = 𝑥𝑏 = 𝑦) → (2nd𝑎) = (2nd𝑥))
2624, 25oveq12d 7449 . . . . . . . . . . . . 13 ((𝑎 = 𝑥𝑏 = 𝑦) → ((1st𝑏) · (2nd𝑎)) = ((1st𝑦) · (2nd𝑥)))
2723, 26oveq12d 7449 . . . . . . . . . . . 12 ((𝑎 = 𝑥𝑏 = 𝑦) → (((1st𝑎) · (2nd𝑏)) ((1st𝑏) · (2nd𝑎))) = (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥))))
2827oveq2d 7447 . . . . . . . . . . 11 ((𝑎 = 𝑥𝑏 = 𝑦) → (𝑡 · (((1st𝑎) · (2nd𝑏)) ((1st𝑏) · (2nd𝑎)))) = (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))))
2928eqeq1d 2739 . . . . . . . . . 10 ((𝑎 = 𝑥𝑏 = 𝑦) → ((𝑡 · (((1st𝑎) · (2nd𝑏)) ((1st𝑏) · (2nd𝑎)))) = 0 ↔ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ))
3029rexbidv 3179 . . . . . . . . 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 32619 . . . . . . 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 20243 . . . . . . . . . . . 12 (𝜑𝑅 ∈ Ring)
4039ringgrpd 20239 . . . . . . . . . . 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 8046 . . . . . . . . . . . . 13 (𝑥 ∈ (𝐵 × 𝑆) → (1st𝑥) ∈ 𝐵)
4544, 9eleq2s 2859 . . . . . . . . . . . 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 8047 . . . . . . . . . . . . . 14 (𝑦 ∈ (𝐵 × 𝑆) → (2nd𝑦) ∈ 𝑆)
5049, 9eleq2s 2859 . . . . . . . . . . . . 13 (𝑦𝑊 → (2nd𝑦) ∈ 𝑆)
5148, 50syl 17 . . . . . . . . . . . 12 ((((𝜑𝑥 𝑦) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) → (2nd𝑦) ∈ 𝑆)
5247, 51sseldd 3984 . . . . . . . . . . 11 ((((𝜑𝑥 𝑦) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) → (2nd𝑦) ∈ 𝐵)
535, 7, 42, 46, 52ringcld 20257 . . . . . . . . . 10 ((((𝜑𝑥 𝑦) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) → ((1st𝑥) · (2nd𝑦)) ∈ 𝐵)
54 xp1st 8046 . . . . . . . . . . . . 13 (𝑦 ∈ (𝐵 × 𝑆) → (1st𝑦) ∈ 𝐵)
5554, 9eleq2s 2859 . . . . . . . . . . . 12 (𝑦𝑊 → (1st𝑦) ∈ 𝐵)
5648, 55syl 17 . . . . . . . . . . 11 ((((𝜑𝑥 𝑦) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) → (1st𝑦) ∈ 𝐵)
57 xp2nd 8047 . . . . . . . . . . . . . 14 (𝑥 ∈ (𝐵 × 𝑆) → (2nd𝑥) ∈ 𝑆)
5857, 9eleq2s 2859 . . . . . . . . . . . . 13 (𝑥𝑊 → (2nd𝑥) ∈ 𝑆)
5943, 58syl 17 . . . . . . . . . . . 12 ((((𝜑𝑥 𝑦) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) → (2nd𝑥) ∈ 𝑆)
6047, 59sseldd 3984 . . . . . . . . . . 11 ((((𝜑𝑥 𝑦) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) → (2nd𝑥) ∈ 𝐵)
615, 7, 42, 56, 60ringcld 20257 . . . . . . . . . 10 ((((𝜑𝑥 𝑦) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) → ((1st𝑦) · (2nd𝑥)) ∈ 𝐵)
62 eqid 2737 . . . . . . . . . . 11 (invg𝑅) = (invg𝑅)
635, 8, 62grpinvsub 19040 . . . . . . . . . 10 ((𝑅 ∈ Grp ∧ ((1st𝑥) · (2nd𝑦)) ∈ 𝐵 ∧ ((1st𝑦) · (2nd𝑥)) ∈ 𝐵) → ((invg𝑅)‘(((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = (((1st𝑦) · (2nd𝑥)) ((1st𝑥) · (2nd𝑦))))
6441, 53, 61, 63syl3anc 1373 . . . . . . . . 9 ((((𝜑𝑥 𝑦) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) → ((invg𝑅)‘(((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = (((1st𝑦) · (2nd𝑥)) ((1st𝑥) · (2nd𝑦))))
6564oveq2d 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 ) → 𝑡𝑆)
6747, 66sseldd 3984 . . . . . . . . . 10 ((((𝜑𝑥 𝑦) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) → 𝑡𝐵)
685, 8grpsubcl 19038 . . . . . . . . . . 11 ((𝑅 ∈ Grp ∧ ((1st𝑥) · (2nd𝑦)) ∈ 𝐵 ∧ ((1st𝑦) · (2nd𝑥)) ∈ 𝐵) → (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥))) ∈ 𝐵)
6941, 53, 61, 68syl3anc 1373 . . . . . . . . . 10 ((((𝜑𝑥 𝑦) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) → (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥))) ∈ 𝐵)
705, 7, 62, 42, 67, 69ringmneg2 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 )
7271fveq2d 6910 . . . . . . . . 9 ((((𝜑𝑥 𝑦) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) → ((invg𝑅)‘(𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥))))) = ((invg𝑅)‘ 0 ))
736, 62grpinvid 19017 . . . . . . . . . 10 (𝑅 ∈ Grp → ((invg𝑅)‘ 0 ) = 0 )
7441, 73syl 17 . . . . . . . . 9 ((((𝜑𝑥 𝑦) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) → ((invg𝑅)‘ 0 ) = 0 )
7570, 72, 743eqtrd 2781 . . . . . . . 8 ((((𝜑𝑥 𝑦) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) → (𝑡 · ((invg𝑅)‘(((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥))))) = 0 )
7665, 75eqtr3d 2779 . . . . . . 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 3168 . . . . 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 7449 . . . . . . . . . 10 ((𝑎 = 𝑦𝑏 = 𝑥) → ((1st𝑎) · (2nd𝑏)) = ((1st𝑦) · (2nd𝑥)))
8683fveq2d 6910 . . . . . . . . . . 11 ((𝑎 = 𝑦𝑏 = 𝑥) → (1st𝑏) = (1st𝑥))
8781fveq2d 6910 . . . . . . . . . . 11 ((𝑎 = 𝑦𝑏 = 𝑥) → (2nd𝑎) = (2nd𝑦))
8886, 87oveq12d 7449 . . . . . . . . . 10 ((𝑎 = 𝑦𝑏 = 𝑥) → ((1st𝑏) · (2nd𝑎)) = ((1st𝑥) · (2nd𝑦)))
8985, 88oveq12d 7449 . . . . . . . . 9 ((𝑎 = 𝑦𝑏 = 𝑥) → (((1st𝑎) · (2nd𝑏)) ((1st𝑏) · (2nd𝑎))) = (((1st𝑦) · (2nd𝑥)) ((1st𝑥) · (2nd𝑦))))
9089oveq2d 7447 . . . . . . . 8 ((𝑎 = 𝑦𝑏 = 𝑥) → (𝑡 · (((1st𝑎) · (2nd𝑏)) ((1st𝑏) · (2nd𝑎)))) = (𝑡 · (((1st𝑦) · (2nd𝑥)) ((1st𝑥) · (2nd𝑦)))))
9190eqeq1d 2739 . . . . . . 7 ((𝑎 = 𝑦𝑏 = 𝑥) → ((𝑡 · (((1st𝑎) · (2nd𝑏)) ((1st𝑏) · (2nd𝑎)))) = 0 ↔ (𝑡 · (((1st𝑦) · (2nd𝑥)) ((1st𝑥) · (2nd𝑦)))) = 0 ))
9291rexbidv 3179 . . . . . 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 32619 . . . 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 2851 . . . . . . 7 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → 𝑥 ∈ (𝐵 × 𝑆))
102 1st2nd2 8053 . . . . . . 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 7449 . . . . . . . . . . . . . . . . . . 19 ((𝑎 = 𝑦𝑏 = 𝑧) → ((1st𝑎) · (2nd𝑏)) = ((1st𝑦) · (2nd𝑧)))
109106fveq2d 6910 . . . . . . . . . . . . . . . . . . . 20 ((𝑎 = 𝑦𝑏 = 𝑧) → (1st𝑏) = (1st𝑧))
110104fveq2d 6910 . . . . . . . . . . . . . . . . . . . 20 ((𝑎 = 𝑦𝑏 = 𝑧) → (2nd𝑎) = (2nd𝑦))
111109, 110oveq12d 7449 . . . . . . . . . . . . . . . . . . 19 ((𝑎 = 𝑦𝑏 = 𝑧) → ((1st𝑏) · (2nd𝑎)) = ((1st𝑧) · (2nd𝑦)))
112108, 111oveq12d 7449 . . . . . . . . . . . . . . . . . 18 ((𝑎 = 𝑦𝑏 = 𝑧) → (((1st𝑎) · (2nd𝑏)) ((1st𝑏) · (2nd𝑎))) = (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦))))
113112oveq2d 7447 . . . . . . . . . . . . . . . . 17 ((𝑎 = 𝑦𝑏 = 𝑧) → (𝑡 · (((1st𝑎) · (2nd𝑏)) ((1st𝑏) · (2nd𝑎)))) = (𝑡 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))))
114113eqeq1d 2739 . . . . . . . . . . . . . . . 16 ((𝑎 = 𝑦𝑏 = 𝑧) → ((𝑡 · (((1st𝑎) · (2nd𝑏)) ((1st𝑏) · (2nd𝑎)))) = 0 ↔ (𝑡 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ))
115114rexbidv 3179 . . . . . . . . . . . . . . 15 ((𝑎 = 𝑦𝑏 = 𝑧) → (∃𝑡𝑆 (𝑡 · (((1st𝑎) · (2nd𝑏)) ((1st𝑏) · (2nd𝑎)))) = 0 ↔ ∃𝑡𝑆 (𝑡 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ))
116 oveq1 7438 . . . . . . . . . . . . . . . . 17 (𝑡 = 𝑢 → (𝑡 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))))
117116eqeq1d 2739 . . . . . . . . . . . . . . . 16 (𝑡 = 𝑢 → ((𝑡 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ↔ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ))
118117cbvrexvw 3238 . . . . . . . . . . . . . . 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 32619 . . . . . . . . . . . 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 2851 . . . . . . 7 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → 𝑧 ∈ (𝐵 × 𝑆))
127 1st2nd2 8053 . . . . . . 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 8046 . . . . . . . 8 (𝑧 ∈ (𝐵 × 𝑆) → (1st𝑧) ∈ 𝐵)
131130, 9eleq2s 2859 . . . . . . 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 8047 . . . . . . . 8 (𝑧 ∈ (𝐵 × 𝑆) → (2nd𝑧) ∈ 𝑆)
135134, 9eleq2s 2859 . . . . . . 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 20141 . . . . . . . . 9 · = (+g‘(mulGrp‘𝑅))
140139submcl 18825 . . . . . . . 8 ((𝑆 ∈ (SubMnd‘(mulGrp‘𝑅)) ∧ 𝑡𝑆𝑢𝑆) → (𝑡 · 𝑢) ∈ 𝑆)
14197, 137, 138, 140syl3anc 1373 . . . . . . 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 18825 . . . . . . 7 ((𝑆 ∈ (SubMnd‘(mulGrp‘𝑅)) ∧ (𝑡 · 𝑢) ∈ 𝑆 ∧ (2nd𝑦) ∈ 𝑆) → ((𝑡 · 𝑢) · (2nd𝑦)) ∈ 𝑆)
14597, 141, 143, 144syl3anc 1373 . . . . . 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 3984 . . . . . . . . . . 11 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → (2nd𝑦) ∈ 𝐵)
14898, 136sseldd 3984 . . . . . . . . . . . 12 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → (2nd𝑧) ∈ 𝐵)
1495, 7, 146, 129, 148ringcld 20257 . . . . . . . . . . 11 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → ((1st𝑥) · (2nd𝑧)) ∈ 𝐵)
15098, 133sseldd 3984 . . . . . . . . . . . 12 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → (2nd𝑥) ∈ 𝐵)
1515, 7, 146, 132, 150ringcld 20257 . . . . . . . . . . 11 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → ((1st𝑧) · (2nd𝑥)) ∈ 𝐵)
1525, 7, 8, 146, 147, 149, 151ringsubdi 20304 . . . . . . . . . 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 20255 . . . . . . . . . . . 12 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → ((2nd𝑦) · ((1st𝑥) · (2nd𝑧))) = ((1st𝑥) · ((2nd𝑦) · (2nd𝑧))))
1555, 7, 153, 147, 148crngcomd 20252 . . . . . . . . . . . . 13 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → ((2nd𝑦) · (2nd𝑧)) = ((2nd𝑧) · (2nd𝑦)))
156155oveq2d 7447 . . . . . . . . . . . 12 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → ((1st𝑥) · ((2nd𝑦) · (2nd𝑧))) = ((1st𝑥) · ((2nd𝑧) · (2nd𝑦))))
1575, 7, 153, 129, 148, 147crng12d 20255 . . . . . . . . . . . 12 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → ((1st𝑥) · ((2nd𝑧) · (2nd𝑦))) = ((2nd𝑧) · ((1st𝑥) · (2nd𝑦))))
158154, 156, 1573eqtrd 2781 . . . . . . . . . . 11 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → ((2nd𝑦) · ((1st𝑥) · (2nd𝑧))) = ((2nd𝑧) · ((1st𝑥) · (2nd𝑦))))
1595, 7, 153, 147, 132, 150crng12d 20255 . . . . . . . . . . . 12 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → ((2nd𝑦) · ((1st𝑧) · (2nd𝑥))) = ((1st𝑧) · ((2nd𝑦) · (2nd𝑥))))
1605, 7, 153, 147, 150crngcomd 20252 . . . . . . . . . . . . 13 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → ((2nd𝑦) · (2nd𝑥)) = ((2nd𝑥) · (2nd𝑦)))
161160oveq2d 7447 . . . . . . . . . . . 12 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → ((1st𝑧) · ((2nd𝑦) · (2nd𝑥))) = ((1st𝑧) · ((2nd𝑥) · (2nd𝑦))))
1625, 7, 153, 132, 150, 147crng12d 20255 . . . . . . . . . . . 12 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → ((1st𝑧) · ((2nd𝑥) · (2nd𝑦))) = ((2nd𝑥) · ((1st𝑧) · (2nd𝑦))))
163159, 161, 1623eqtrd 2781 . . . . . . . . . . 11 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → ((2nd𝑦) · ((1st𝑧) · (2nd𝑥))) = ((2nd𝑥) · ((1st𝑧) · (2nd𝑦))))
164158, 163oveq12d 7449 . . . . . . . . . 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 20257 . . . . . . . . . . . . 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 20257 . . . . . . . . . . . . 13 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → ((1st𝑦) · (2nd𝑥)) ∈ 𝐵)
1685, 7, 8, 146, 148, 165, 167ringsubdi 20304 . . . . . . . . . . . 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 20257 . . . . . . . . . . . . 13 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → ((1st𝑦) · (2nd𝑧)) ∈ 𝐵)
1705, 7, 146, 132, 147ringcld 20257 . . . . . . . . . . . . 13 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → ((1st𝑧) · (2nd𝑦)) ∈ 𝐵)
1715, 7, 8, 146, 150, 169, 170ringsubdi 20304 . . . . . . . . . . . 12 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → ((2nd𝑥) · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = (((2nd𝑥) · ((1st𝑦) · (2nd𝑧))) ((2nd𝑥) · ((1st𝑧) · (2nd𝑦)))))
172168, 171oveq12d 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𝑦))))))
1735, 7, 153, 166, 148, 150crng12d 20255 . . . . . . . . . . . . 13 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → ((1st𝑦) · ((2nd𝑧) · (2nd𝑥))) = ((2nd𝑧) · ((1st𝑦) · (2nd𝑥))))
174173oveq2d 7447 . . . . . . . . . . . 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 20252 . . . . . . . . . . . . . . 15 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → ((2nd𝑧) · (2nd𝑥)) = ((2nd𝑥) · (2nd𝑧)))
176175oveq2d 7447 . . . . . . . . . . . . . 14 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → ((1st𝑦) · ((2nd𝑧) · (2nd𝑥))) = ((1st𝑦) · ((2nd𝑥) · (2nd𝑧))))
1775, 7, 153, 150, 166, 148crng12d 20255 . . . . . . . . . . . . . 14 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → ((2nd𝑥) · ((1st𝑦) · (2nd𝑧))) = ((1st𝑦) · ((2nd𝑥) · (2nd𝑧))))
178176, 177eqtr4d 2780 . . . . . . . . . . . . 13 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → ((1st𝑦) · ((2nd𝑧) · (2nd𝑥))) = ((2nd𝑥) · ((1st𝑦) · (2nd𝑧))))
179178oveq1d 7446 . . . . . . . . . . . 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 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𝑦))))))
18140ad6antr 736 . . . . . . . . . . . 12 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → 𝑅 ∈ Grp)
1825, 7, 146, 148, 165ringcld 20257 . . . . . . . . . . . 12 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → ((2nd𝑧) · ((1st𝑥) · (2nd𝑦))) ∈ 𝐵)
1835, 7, 146, 148, 150ringcld 20257 . . . . . . . . . . . . 13 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → ((2nd𝑧) · (2nd𝑥)) ∈ 𝐵)
1845, 7, 146, 166, 183ringcld 20257 . . . . . . . . . . . 12 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → ((1st𝑦) · ((2nd𝑧) · (2nd𝑥))) ∈ 𝐵)
1855, 7, 146, 150, 170ringcld 20257 . . . . . . . . . . . 12 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → ((2nd𝑥) · ((1st𝑧) · (2nd𝑦))) ∈ 𝐵)
186 eqid 2737 . . . . . . . . . . . . 13 (+g𝑅) = (+g𝑅)
1875, 186, 8grpnpncan 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𝑦)))))
188181, 182, 184, 185, 187syl13anc 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𝑦)))))
189172, 180, 1883eqtr2rd 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𝑦))))))
190152, 164, 1893eqtrd 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𝑦))))))
191190oveq2d 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𝑦)))))))
19298, 141sseldd 3984 . . . . . . . . 9 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → (𝑡 · 𝑢) ∈ 𝐵)
1935, 8grpsubcl 19038 . . . . . . . . . 10 ((𝑅 ∈ Grp ∧ ((1st𝑥) · (2nd𝑧)) ∈ 𝐵 ∧ ((1st𝑧) · (2nd𝑥)) ∈ 𝐵) → (((1st𝑥) · (2nd𝑧)) ((1st𝑧) · (2nd𝑥))) ∈ 𝐵)
194181, 149, 151, 193syl3anc 1373 . . . . . . . . 9 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → (((1st𝑥) · (2nd𝑧)) ((1st𝑧) · (2nd𝑥))) ∈ 𝐵)
1955, 7, 146, 192, 147, 194ringassd 20254 . . . . . . . 8 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → (((𝑡 · 𝑢) · (2nd𝑦)) · (((1st𝑥) · (2nd𝑧)) ((1st𝑧) · (2nd𝑥)))) = ((𝑡 · 𝑢) · ((2nd𝑦) · (((1st𝑥) · (2nd𝑧)) ((1st𝑧) · (2nd𝑥))))))
19698, 138sseldd 3984 . . . . . . . . . . . . . 14 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → 𝑢𝐵)
19798, 137sseldd 3984 . . . . . . . . . . . . . 14 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → 𝑡𝐵)
1985, 7, 153, 196, 148, 197crng32d 20256 . . . . . . . . . . . . 13 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → ((𝑢 · (2nd𝑧)) · 𝑡) = ((𝑢 · 𝑡) · (2nd𝑧)))
1995, 7, 153, 196, 197crngcomd 20252 . . . . . . . . . . . . . 14 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → (𝑢 · 𝑡) = (𝑡 · 𝑢))
200199oveq1d 7446 . . . . . . . . . . . . 13 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → ((𝑢 · 𝑡) · (2nd𝑧)) = ((𝑡 · 𝑢) · (2nd𝑧)))
201198, 200eqtrd 2777 . . . . . . . . . . . 12 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → ((𝑢 · (2nd𝑧)) · 𝑡) = ((𝑡 · 𝑢) · (2nd𝑧)))
202201oveq1d 7446 . . . . . . . . . . 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 20257 . . . . . . . . . . . 12 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → (𝑢 · (2nd𝑧)) ∈ 𝐵)
204181, 165, 167, 68syl3anc 1373 . . . . . . . . . . . 12 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥))) ∈ 𝐵)
2055, 7, 146, 203, 197, 204ringassd 20254 . . . . . . . . . . 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 20254 . . . . . . . . . . 11 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → (((𝑡 · 𝑢) · (2nd𝑧)) · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = ((𝑡 · 𝑢) · ((2nd𝑧) · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥))))))
207202, 205, 2063eqtr3d 2785 . . . . . . . . . 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, 196crng32d 20256 . . . . . . . . . . . 12 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → ((𝑡 · (2nd𝑥)) · 𝑢) = ((𝑡 · 𝑢) · (2nd𝑥)))
209208oveq1d 7446 . . . . . . . . . . 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 20257 . . . . . . . . . . . 12 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → (𝑡 · (2nd𝑥)) ∈ 𝐵)
2115, 8grpsubcl 19038 . . . . . . . . . . . . 13 ((𝑅 ∈ Grp ∧ ((1st𝑦) · (2nd𝑧)) ∈ 𝐵 ∧ ((1st𝑧) · (2nd𝑦)) ∈ 𝐵) → (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦))) ∈ 𝐵)
212181, 169, 170, 211syl3anc 1373 . . . . . . . . . . . 12 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦))) ∈ 𝐵)
2135, 7, 146, 210, 196, 212ringassd 20254 . . . . . . . . . . 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 20254 . . . . . . . . . . 11 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → (((𝑡 · 𝑢) · (2nd𝑥)) · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = ((𝑡 · 𝑢) · ((2nd𝑥) · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦))))))
215209, 213, 2143eqtr3d 2785 . . . . . . . . . 10 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → ((𝑡 · (2nd𝑥)) · (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦))))) = ((𝑡 · 𝑢) · ((2nd𝑥) · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦))))))
216207, 215oveq12d 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𝑦)))))))
2175, 7, 146, 148, 204ringcld 20257 . . . . . . . . . 10 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → ((2nd𝑧) · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) ∈ 𝐵)
2185, 7, 146, 150, 212ringcld 20257 . . . . . . . . . 10 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → ((2nd𝑥) · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) ∈ 𝐵)
2195, 186, 7ringdi 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𝑦)))))))
220146, 192, 217, 218, 219syl13anc 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𝑦)))))))
221216, 220eqtr4d 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𝑦)))))))
222191, 195, 2213eqtr4d 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 )
224223oveq2d 7447 . . . . . . . . 9 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → ((𝑢 · (2nd𝑧)) · (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥))))) = ((𝑢 · (2nd𝑧)) · 0 ))
2255, 7, 6, 146, 203ringrzd 20293 . . . . . . . . 9 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → ((𝑢 · (2nd𝑧)) · 0 ) = 0 )
226224, 225eqtrd 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 )
228227oveq2d 7447 . . . . . . . . 9 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → ((𝑡 · (2nd𝑥)) · (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦))))) = ((𝑡 · (2nd𝑥)) · 0 ))
2295, 7, 6, 146, 210ringrzd 20293 . . . . . . . . 9 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → ((𝑡 · (2nd𝑥)) · 0 ) = 0 )
230228, 229eqtrd 2777 . . . . . . . 8 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → ((𝑡 · (2nd𝑥)) · (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦))))) = 0 )
231226, 230oveq12d 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 ))
2325, 6grpidcl 18983 . . . . . . . . 9 (𝑅 ∈ Grp → 0𝐵)
233181, 232syl 17 . . . . . . . 8 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → 0𝐵)
2345, 186, 6, 181, 233grplidd 18987 . . . . . . 7 (((((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) ∧ 𝑢𝑆) ∧ (𝑢 · (((1st𝑦) · (2nd𝑧)) ((1st𝑧) · (2nd𝑦)))) = 0 ) → ( 0 (+g𝑅) 0 ) = 0 )
235222, 231, 2343eqtrd 2781 . . . . . 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 33267 . . . . 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 3162 . . . 4 (((((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) ∧ 𝑡𝑆) ∧ (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 ) → 𝑥 𝑧)
24037adantr 480 . . . 4 (((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) → ∃𝑡𝑆 (𝑡 · (((1st𝑥) · (2nd𝑦)) ((1st𝑦) · (2nd𝑥)))) = 0 )
241239, 240r19.29a 3162 . . 3 (((𝜑𝑥 𝑦) ∧ 𝑦 𝑧) → 𝑥 𝑧)
242241anasss 466 . 2 ((𝜑 ∧ (𝑥 𝑦𝑦 𝑧)) → 𝑥 𝑧)
243 erler.3 . . . . . . . . . . 11 1 = (1r𝑅)
24411, 243ringidval 20180 . . . . . . . . . 10 1 = (0g‘(mulGrp‘𝑅))
245244subm0cl 18824 . . . . . . . . 9 (𝑆 ∈ (SubMnd‘(mulGrp‘𝑅)) → 1𝑆)
24610, 245syl 17 . . . . . . . 8 (𝜑1𝑆)
247246adantr 480 . . . . . . 7 ((𝜑𝑥𝑊) → 1𝑆)
248 oveq1 7438 . . . . . . . . 9 (𝑡 = 1 → (𝑡 · (((1st𝑥) · (2nd𝑥)) ((1st𝑥) · (2nd𝑥)))) = ( 1 · (((1st𝑥) · (2nd𝑥)) ((1st𝑥) · (2nd𝑥)))))
249248eqeq1d 2739 . . . . . . . 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 3984 . . . . . . . . . . 11 ((𝜑𝑥𝑊) → (2nd𝑥) ∈ 𝐵)
2565, 7, 251, 252, 255ringcld 20257 . . . . . . . . . 10 ((𝜑𝑥𝑊) → ((1st𝑥) · (2nd𝑥)) ∈ 𝐵)
2575, 6, 8grpsubid 19042 . . . . . . . . . 10 ((𝑅 ∈ Grp ∧ ((1st𝑥) · (2nd𝑥)) ∈ 𝐵) → (((1st𝑥) · (2nd𝑥)) ((1st𝑥) · (2nd𝑥))) = 0 )
25840, 256, 257syl2an2r 685 . . . . . . . . 9 ((𝜑𝑥𝑊) → (((1st𝑥) · (2nd𝑥)) ((1st𝑥) · (2nd𝑥))) = 0 )
259258oveq2d 7447 . . . . . . . 8 ((𝜑𝑥𝑊) → ( 1 · (((1st𝑥) · (2nd𝑥)) ((1st𝑥) · (2nd𝑥)))) = ( 1 · 0 ))
26040, 232syl 17 . . . . . . . . . 10 (𝜑0𝐵)
2615, 7, 243, 39, 260ringlidmd 20269 . . . . . . . . 9 (𝜑 → ( 1 · 0 ) = 0 )
262261adantr 480 . . . . . . . 8 ((𝜑𝑥𝑊) → ( 1 · 0 ) = 0 )
263259, 262eqtrd 2777 . . . . . . 7 ((𝜑𝑥𝑊) → ( 1 · (((1st𝑥) · (2nd𝑥)) ((1st𝑥) · (2nd𝑥)))) = 0 )
264247, 250, 263rspcedvd 3624 . . . . . 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 7449 . . . . . . . . 9 ((𝑎 = 𝑥𝑏 = 𝑥) → ((1st𝑎) · (2nd𝑏)) = ((1st𝑥) · (2nd𝑥)))
275272fveq2d 6910 . . . . . . . . . 10 ((𝑎 = 𝑥𝑏 = 𝑥) → (1st𝑏) = (1st𝑥))
276270fveq2d 6910 . . . . . . . . . 10 ((𝑎 = 𝑥𝑏 = 𝑥) → (2nd𝑎) = (2nd𝑥))
277275, 276oveq12d 7449 . . . . . . . . 9 ((𝑎 = 𝑥𝑏 = 𝑥) → ((1st𝑏) · (2nd𝑎)) = ((1st𝑥) · (2nd𝑥)))
278274, 277oveq12d 7449 . . . . . . . 8 ((𝑎 = 𝑥𝑏 = 𝑥) → (((1st𝑎) · (2nd𝑏)) ((1st𝑏) · (2nd𝑎))) = (((1st𝑥) · (2nd𝑥)) ((1st𝑥) · (2nd𝑥))))
279278oveq2d 7447 . . . . . . 7 ((𝑎 = 𝑥𝑏 = 𝑥) → (𝑡 · (((1st𝑎) · (2nd𝑏)) ((1st𝑏) · (2nd𝑎)))) = (𝑡 · (((1st𝑥) · (2nd𝑥)) ((1st𝑥) · (2nd𝑥)))))
280279eqeq1d 2739 . . . . . 6 ((𝑎 = 𝑥𝑏 = 𝑥) → ((𝑡 · (((1st𝑎) · (2nd𝑏)) ((1st𝑏) · (2nd𝑎)))) = 0 ↔ (𝑡 · (((1st𝑥) · (2nd𝑥)) ((1st𝑥) · (2nd𝑥)))) = 0 ))
281280rexbidv 3179 . . . . 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 32619 . . 3 (𝜑 → (𝑥 𝑥 ↔ ((𝑥𝑊𝑥𝑊) ∧ ∃𝑡𝑆 (𝑡 · (((1st𝑥) · (2nd𝑥)) ((1st𝑥) · (2nd𝑥)))) = 0 )))
284269, 283bitr4d 282 . 2 (𝜑 → (𝑥𝑊𝑥 𝑥))
28518, 96, 242, 284iserd 8771 1 (𝜑 Er 𝑊)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395   = wceq 1540  wcel 2108  wrex 3070  wss 3951  cop 4632   class class class wbr 5143  {copab 5205   × cxp 5683  Rel wrel 5690  cfv 6561  (class class class)co 7431  1st c1st 8012  2nd c2nd 8013   Er wer 8742  Basecbs 17247  +gcplusg 17297  .rcmulr 17298  0gc0g 17484  SubMndcsubmnd 18795  Grpcgrp 18951  invgcminusg 18952  -gcsg 18953  mulGrpcmgp 20137  1rcur 20178  Ringcrg 20230  CRingccrg 20231   ~RL cerl 33257
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-cnex 11211  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-mulcom 11219  ax-addass 11220  ax-mulass 11221  ax-distr 11222  ax-i2m1 11223  ax-1ne0 11224  ax-1rid 11225  ax-rnegex 11226  ax-rrecex 11227  ax-cnre 11228  ax-pre-lttri 11229  ax-pre-lttrn 11230  ax-pre-ltadd 11231  ax-pre-mulgt0 11232
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-1st 8014  df-2nd 8015  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-er 8745  df-en 8986  df-dom 8987  df-sdom 8988  df-pnf 11297  df-mnf 11298  df-xr 11299  df-ltxr 11300  df-le 11301  df-sub 11494  df-neg 11495  df-nn 12267  df-2 12329  df-sets 17201  df-slot 17219  df-ndx 17231  df-base 17248  df-ress 17275  df-plusg 17310  df-0g 17486  df-mgm 18653  df-sgrp 18732  df-mnd 18748  df-submnd 18797  df-grp 18954  df-minusg 18955  df-sbg 18956  df-cmn 19800  df-abl 19801  df-mgp 20138  df-rng 20150  df-ur 20179  df-ring 20232  df-cring 20233  df-erl 33259
This theorem is referenced by:  rlocaddval  33272  rlocmulval  33273  rloccring  33274  rlocf1  33277  fracfld  33310  zringfrac  33582
  Copyright terms: Public domain W3C validator