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

Theorem erlbrd 33250
Description: Deduce the ring localization equivalence relation. If for some 𝑇𝑆 we have 𝑇 · (𝐸 · 𝐻𝐹 · 𝐺) = 0, then pairs 𝐸, 𝐺 and 𝐹, 𝐻 are equivalent under the localization relation. (Contributed by Thierry Arnoux, 4-May-2025.)
Hypotheses
Ref Expression
erlcl1.b 𝐵 = (Base‘𝑅)
erlcl1.e = (𝑅 ~RL 𝑆)
erlcl1.s (𝜑𝑆𝐵)
erldi.1 0 = (0g𝑅)
erldi.2 · = (.r𝑅)
erldi.3 = (-g𝑅)
erlbrd.u (𝜑𝑈 = ⟨𝐸, 𝐺⟩)
erlbrd.v (𝜑𝑉 = ⟨𝐹, 𝐻⟩)
erlbrd.e (𝜑𝐸𝐵)
erlbrd.f (𝜑𝐹𝐵)
erlbrd.g (𝜑𝐺𝑆)
erlbrd.h (𝜑𝐻𝑆)
erlbrd.1 (𝜑𝑇𝑆)
erlbrd.2 (𝜑 → (𝑇 · ((𝐸 · 𝐻) (𝐹 · 𝐺))) = 0 )
Assertion
Ref Expression
erlbrd (𝜑𝑈 𝑉)

Proof of Theorem erlbrd
Dummy variables 𝑎 𝑏 𝑡 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 erlbrd.u . . . . 5 (𝜑𝑈 = ⟨𝐸, 𝐺⟩)
2 erlbrd.e . . . . . 6 (𝜑𝐸𝐵)
3 erlbrd.g . . . . . 6 (𝜑𝐺𝑆)
42, 3opelxpd 5728 . . . . 5 (𝜑 → ⟨𝐸, 𝐺⟩ ∈ (𝐵 × 𝑆))
51, 4eqeltrd 2839 . . . 4 (𝜑𝑈 ∈ (𝐵 × 𝑆))
6 erlbrd.v . . . . 5 (𝜑𝑉 = ⟨𝐹, 𝐻⟩)
7 erlbrd.f . . . . . 6 (𝜑𝐹𝐵)
8 erlbrd.h . . . . . 6 (𝜑𝐻𝑆)
97, 8opelxpd 5728 . . . . 5 (𝜑 → ⟨𝐹, 𝐻⟩ ∈ (𝐵 × 𝑆))
106, 9eqeltrd 2839 . . . 4 (𝜑𝑉 ∈ (𝐵 × 𝑆))
115, 10jca 511 . . 3 (𝜑 → (𝑈 ∈ (𝐵 × 𝑆) ∧ 𝑉 ∈ (𝐵 × 𝑆)))
12 erlbrd.1 . . . 4 (𝜑𝑇𝑆)
13 simpr 484 . . . . . 6 ((𝜑𝑡 = 𝑇) → 𝑡 = 𝑇)
1413oveq1d 7446 . . . . 5 ((𝜑𝑡 = 𝑇) → (𝑡 · ((𝐸 · 𝐻) (𝐹 · 𝐺))) = (𝑇 · ((𝐸 · 𝐻) (𝐹 · 𝐺))))
1514eqeq1d 2737 . . . 4 ((𝜑𝑡 = 𝑇) → ((𝑡 · ((𝐸 · 𝐻) (𝐹 · 𝐺))) = 0 ↔ (𝑇 · ((𝐸 · 𝐻) (𝐹 · 𝐺))) = 0 ))
16 erlbrd.2 . . . 4 (𝜑 → (𝑇 · ((𝐸 · 𝐻) (𝐹 · 𝐺))) = 0 )
1712, 15, 16rspcedvd 3624 . . 3 (𝜑 → ∃𝑡𝑆 (𝑡 · ((𝐸 · 𝐻) (𝐹 · 𝐺))) = 0 )
1811, 17jca 511 . 2 (𝜑 → ((𝑈 ∈ (𝐵 × 𝑆) ∧ 𝑉 ∈ (𝐵 × 𝑆)) ∧ ∃𝑡𝑆 (𝑡 · ((𝐸 · 𝐻) (𝐹 · 𝐺))) = 0 ))
19 erlcl1.e . . . 4 = (𝑅 ~RL 𝑆)
20 erlcl1.b . . . . 5 𝐵 = (Base‘𝑅)
21 erldi.1 . . . . 5 0 = (0g𝑅)
22 erldi.2 . . . . 5 · = (.r𝑅)
23 erldi.3 . . . . 5 = (-g𝑅)
24 eqid 2735 . . . . 5 (𝐵 × 𝑆) = (𝐵 × 𝑆)
25 eqid 2735 . . . . 5 {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝐵 × 𝑆) ∧ 𝑏 ∈ (𝐵 × 𝑆)) ∧ ∃𝑡𝑆 (𝑡 · (((1st𝑎) · (2nd𝑏)) ((1st𝑏) · (2nd𝑎)))) = 0 )} = {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝐵 × 𝑆) ∧ 𝑏 ∈ (𝐵 × 𝑆)) ∧ ∃𝑡𝑆 (𝑡 · (((1st𝑎) · (2nd𝑏)) ((1st𝑏) · (2nd𝑎)))) = 0 )}
26 erlcl1.s . . . . 5 (𝜑𝑆𝐵)
2720, 21, 22, 23, 24, 25, 26erlval 33245 . . . 4 (𝜑 → (𝑅 ~RL 𝑆) = {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝐵 × 𝑆) ∧ 𝑏 ∈ (𝐵 × 𝑆)) ∧ ∃𝑡𝑆 (𝑡 · (((1st𝑎) · (2nd𝑏)) ((1st𝑏) · (2nd𝑎)))) = 0 )})
2819, 27eqtrid 2787 . . 3 (𝜑 = {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝐵 × 𝑆) ∧ 𝑏 ∈ (𝐵 × 𝑆)) ∧ ∃𝑡𝑆 (𝑡 · (((1st𝑎) · (2nd𝑏)) ((1st𝑏) · (2nd𝑎)))) = 0 )})
29 simprl 771 . . . . . . . . . 10 ((𝜑 ∧ (𝑎 = 𝑈𝑏 = 𝑉)) → 𝑎 = 𝑈)
3029fveq2d 6911 . . . . . . . . 9 ((𝜑 ∧ (𝑎 = 𝑈𝑏 = 𝑉)) → (1st𝑎) = (1st𝑈))
311fveq2d 6911 . . . . . . . . . . 11 (𝜑 → (1st𝑈) = (1st ‘⟨𝐸, 𝐺⟩))
32 op1stg 8025 . . . . . . . . . . . 12 ((𝐸𝐵𝐺𝑆) → (1st ‘⟨𝐸, 𝐺⟩) = 𝐸)
332, 3, 32syl2anc 584 . . . . . . . . . . 11 (𝜑 → (1st ‘⟨𝐸, 𝐺⟩) = 𝐸)
3431, 33eqtrd 2775 . . . . . . . . . 10 (𝜑 → (1st𝑈) = 𝐸)
3534adantr 480 . . . . . . . . 9 ((𝜑 ∧ (𝑎 = 𝑈𝑏 = 𝑉)) → (1st𝑈) = 𝐸)
3630, 35eqtrd 2775 . . . . . . . 8 ((𝜑 ∧ (𝑎 = 𝑈𝑏 = 𝑉)) → (1st𝑎) = 𝐸)
37 simprr 773 . . . . . . . . . 10 ((𝜑 ∧ (𝑎 = 𝑈𝑏 = 𝑉)) → 𝑏 = 𝑉)
3837fveq2d 6911 . . . . . . . . 9 ((𝜑 ∧ (𝑎 = 𝑈𝑏 = 𝑉)) → (2nd𝑏) = (2nd𝑉))
396fveq2d 6911 . . . . . . . . . . 11 (𝜑 → (2nd𝑉) = (2nd ‘⟨𝐹, 𝐻⟩))
40 op2ndg 8026 . . . . . . . . . . . 12 ((𝐹𝐵𝐻𝑆) → (2nd ‘⟨𝐹, 𝐻⟩) = 𝐻)
417, 8, 40syl2anc 584 . . . . . . . . . . 11 (𝜑 → (2nd ‘⟨𝐹, 𝐻⟩) = 𝐻)
4239, 41eqtrd 2775 . . . . . . . . . 10 (𝜑 → (2nd𝑉) = 𝐻)
4342adantr 480 . . . . . . . . 9 ((𝜑 ∧ (𝑎 = 𝑈𝑏 = 𝑉)) → (2nd𝑉) = 𝐻)
4438, 43eqtrd 2775 . . . . . . . 8 ((𝜑 ∧ (𝑎 = 𝑈𝑏 = 𝑉)) → (2nd𝑏) = 𝐻)
4536, 44oveq12d 7449 . . . . . . 7 ((𝜑 ∧ (𝑎 = 𝑈𝑏 = 𝑉)) → ((1st𝑎) · (2nd𝑏)) = (𝐸 · 𝐻))
4637fveq2d 6911 . . . . . . . . 9 ((𝜑 ∧ (𝑎 = 𝑈𝑏 = 𝑉)) → (1st𝑏) = (1st𝑉))
476fveq2d 6911 . . . . . . . . . . 11 (𝜑 → (1st𝑉) = (1st ‘⟨𝐹, 𝐻⟩))
48 op1stg 8025 . . . . . . . . . . . 12 ((𝐹𝐵𝐻𝑆) → (1st ‘⟨𝐹, 𝐻⟩) = 𝐹)
497, 8, 48syl2anc 584 . . . . . . . . . . 11 (𝜑 → (1st ‘⟨𝐹, 𝐻⟩) = 𝐹)
5047, 49eqtrd 2775 . . . . . . . . . 10 (𝜑 → (1st𝑉) = 𝐹)
5150adantr 480 . . . . . . . . 9 ((𝜑 ∧ (𝑎 = 𝑈𝑏 = 𝑉)) → (1st𝑉) = 𝐹)
5246, 51eqtrd 2775 . . . . . . . 8 ((𝜑 ∧ (𝑎 = 𝑈𝑏 = 𝑉)) → (1st𝑏) = 𝐹)
5329fveq2d 6911 . . . . . . . . 9 ((𝜑 ∧ (𝑎 = 𝑈𝑏 = 𝑉)) → (2nd𝑎) = (2nd𝑈))
541fveq2d 6911 . . . . . . . . . . 11 (𝜑 → (2nd𝑈) = (2nd ‘⟨𝐸, 𝐺⟩))
55 op2ndg 8026 . . . . . . . . . . . 12 ((𝐸𝐵𝐺𝑆) → (2nd ‘⟨𝐸, 𝐺⟩) = 𝐺)
562, 3, 55syl2anc 584 . . . . . . . . . . 11 (𝜑 → (2nd ‘⟨𝐸, 𝐺⟩) = 𝐺)
5754, 56eqtrd 2775 . . . . . . . . . 10 (𝜑 → (2nd𝑈) = 𝐺)
5857adantr 480 . . . . . . . . 9 ((𝜑 ∧ (𝑎 = 𝑈𝑏 = 𝑉)) → (2nd𝑈) = 𝐺)
5953, 58eqtrd 2775 . . . . . . . 8 ((𝜑 ∧ (𝑎 = 𝑈𝑏 = 𝑉)) → (2nd𝑎) = 𝐺)
6052, 59oveq12d 7449 . . . . . . 7 ((𝜑 ∧ (𝑎 = 𝑈𝑏 = 𝑉)) → ((1st𝑏) · (2nd𝑎)) = (𝐹 · 𝐺))
6145, 60oveq12d 7449 . . . . . 6 ((𝜑 ∧ (𝑎 = 𝑈𝑏 = 𝑉)) → (((1st𝑎) · (2nd𝑏)) ((1st𝑏) · (2nd𝑎))) = ((𝐸 · 𝐻) (𝐹 · 𝐺)))
6261oveq2d 7447 . . . . 5 ((𝜑 ∧ (𝑎 = 𝑈𝑏 = 𝑉)) → (𝑡 · (((1st𝑎) · (2nd𝑏)) ((1st𝑏) · (2nd𝑎)))) = (𝑡 · ((𝐸 · 𝐻) (𝐹 · 𝐺))))
6362eqeq1d 2737 . . . 4 ((𝜑 ∧ (𝑎 = 𝑈𝑏 = 𝑉)) → ((𝑡 · (((1st𝑎) · (2nd𝑏)) ((1st𝑏) · (2nd𝑎)))) = 0 ↔ (𝑡 · ((𝐸 · 𝐻) (𝐹 · 𝐺))) = 0 ))
6463rexbidv 3177 . . 3 ((𝜑 ∧ (𝑎 = 𝑈𝑏 = 𝑉)) → (∃𝑡𝑆 (𝑡 · (((1st𝑎) · (2nd𝑏)) ((1st𝑏) · (2nd𝑎)))) = 0 ↔ ∃𝑡𝑆 (𝑡 · ((𝐸 · 𝐻) (𝐹 · 𝐺))) = 0 ))
6528, 64brab2d 32627 . 2 (𝜑 → (𝑈 𝑉 ↔ ((𝑈 ∈ (𝐵 × 𝑆) ∧ 𝑉 ∈ (𝐵 × 𝑆)) ∧ ∃𝑡𝑆 (𝑡 · ((𝐸 · 𝐻) (𝐹 · 𝐺))) = 0 )))
6618, 65mpbird 257 1 (𝜑𝑈 𝑉)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395   = wceq 1537  wcel 2106  wrex 3068  wss 3963  cop 4637   class class class wbr 5148  {copab 5210   × cxp 5687  cfv 6563  (class class class)co 7431  1st c1st 8011  2nd c2nd 8012  Basecbs 17245  .rcmulr 17299  0gc0g 17486  -gcsg 18966   ~RL cerl 33240
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pow 5371  ax-pr 5438  ax-un 7754
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-sbc 3792  df-csb 3909  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5583  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-iota 6516  df-fun 6565  df-fv 6571  df-ov 7434  df-oprab 7435  df-mpo 7436  df-1st 8013  df-2nd 8014  df-erl 33242
This theorem is referenced by:  erlbr2d  33251  erler  33252  rlocaddval  33255  rlocmulval  33256  rloccring  33257
  Copyright terms: Public domain W3C validator