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

Theorem isorng 32417
Description: An ordered ring is a ring with a total ordering compatible with its operations. (Contributed by Thierry Arnoux, 18-Jan-2018.)
Hypotheses
Ref Expression
isorng.0 𝐡 = (Baseβ€˜π‘…)
isorng.1 0 = (0gβ€˜π‘…)
isorng.2 Β· = (.rβ€˜π‘…)
isorng.3 ≀ = (leβ€˜π‘…)
Assertion
Ref Expression
isorng (𝑅 ∈ oRing ↔ (𝑅 ∈ Ring ∧ 𝑅 ∈ oGrp ∧ βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 (( 0 ≀ π‘Ž ∧ 0 ≀ 𝑏) β†’ 0 ≀ (π‘Ž Β· 𝑏))))
Distinct variable groups:   π‘Ž,𝑏,𝐡   𝑅,π‘Ž,𝑏
Allowed substitution hints:   Β· (π‘Ž,𝑏)   ≀ (π‘Ž,𝑏)   0 (π‘Ž,𝑏)

Proof of Theorem isorng
Dummy variables 𝑙 π‘Ÿ 𝑑 𝑣 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elin 3965 . . 3 (𝑅 ∈ (Ring ∩ oGrp) ↔ (𝑅 ∈ Ring ∧ 𝑅 ∈ oGrp))
21anbi1i 625 . 2 ((𝑅 ∈ (Ring ∩ oGrp) ∧ βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 (( 0 ≀ π‘Ž ∧ 0 ≀ 𝑏) β†’ 0 ≀ (π‘Ž Β· 𝑏))) ↔ ((𝑅 ∈ Ring ∧ 𝑅 ∈ oGrp) ∧ βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 (( 0 ≀ π‘Ž ∧ 0 ≀ 𝑏) β†’ 0 ≀ (π‘Ž Β· 𝑏))))
3 fvexd 6907 . . . . 5 (π‘Ÿ = 𝑅 β†’ (.rβ€˜π‘Ÿ) ∈ V)
4 simpr 486 . . . . . . . . . . 11 ((π‘Ÿ = 𝑅 ∧ 𝑑 = (.rβ€˜π‘Ÿ)) β†’ 𝑑 = (.rβ€˜π‘Ÿ))
5 simpl 484 . . . . . . . . . . . . 13 ((π‘Ÿ = 𝑅 ∧ 𝑑 = (.rβ€˜π‘Ÿ)) β†’ π‘Ÿ = 𝑅)
65fveq2d 6896 . . . . . . . . . . . 12 ((π‘Ÿ = 𝑅 ∧ 𝑑 = (.rβ€˜π‘Ÿ)) β†’ (.rβ€˜π‘Ÿ) = (.rβ€˜π‘…))
7 isorng.2 . . . . . . . . . . . 12 Β· = (.rβ€˜π‘…)
86, 7eqtr4di 2791 . . . . . . . . . . 11 ((π‘Ÿ = 𝑅 ∧ 𝑑 = (.rβ€˜π‘Ÿ)) β†’ (.rβ€˜π‘Ÿ) = Β· )
94, 8eqtrd 2773 . . . . . . . . . 10 ((π‘Ÿ = 𝑅 ∧ 𝑑 = (.rβ€˜π‘Ÿ)) β†’ 𝑑 = Β· )
109oveqd 7426 . . . . . . . . 9 ((π‘Ÿ = 𝑅 ∧ 𝑑 = (.rβ€˜π‘Ÿ)) β†’ (π‘Žπ‘‘π‘) = (π‘Ž Β· 𝑏))
1110breq2d 5161 . . . . . . . 8 ((π‘Ÿ = 𝑅 ∧ 𝑑 = (.rβ€˜π‘Ÿ)) β†’ ( 0 𝑙(π‘Žπ‘‘π‘) ↔ 0 𝑙(π‘Ž Β· 𝑏)))
1211imbi2d 341 . . . . . . 7 ((π‘Ÿ = 𝑅 ∧ 𝑑 = (.rβ€˜π‘Ÿ)) β†’ ((( 0 π‘™π‘Ž ∧ 0 𝑙𝑏) β†’ 0 𝑙(π‘Žπ‘‘π‘)) ↔ (( 0 π‘™π‘Ž ∧ 0 𝑙𝑏) β†’ 0 𝑙(π‘Ž Β· 𝑏))))
13122ralbidv 3219 . . . . . 6 ((π‘Ÿ = 𝑅 ∧ 𝑑 = (.rβ€˜π‘Ÿ)) β†’ (βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 (( 0 π‘™π‘Ž ∧ 0 𝑙𝑏) β†’ 0 𝑙(π‘Žπ‘‘π‘)) ↔ βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 (( 0 π‘™π‘Ž ∧ 0 𝑙𝑏) β†’ 0 𝑙(π‘Ž Β· 𝑏))))
1413sbcbidv 3837 . . . . 5 ((π‘Ÿ = 𝑅 ∧ 𝑑 = (.rβ€˜π‘Ÿ)) β†’ ([(leβ€˜π‘Ÿ) / 𝑙]βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 (( 0 π‘™π‘Ž ∧ 0 𝑙𝑏) β†’ 0 𝑙(π‘Žπ‘‘π‘)) ↔ [(leβ€˜π‘Ÿ) / 𝑙]βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 (( 0 π‘™π‘Ž ∧ 0 𝑙𝑏) β†’ 0 𝑙(π‘Ž Β· 𝑏))))
153, 14sbcied 3823 . . . 4 (π‘Ÿ = 𝑅 β†’ ([(.rβ€˜π‘Ÿ) / 𝑑][(leβ€˜π‘Ÿ) / 𝑙]βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 (( 0 π‘™π‘Ž ∧ 0 𝑙𝑏) β†’ 0 𝑙(π‘Žπ‘‘π‘)) ↔ [(leβ€˜π‘Ÿ) / 𝑙]βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 (( 0 π‘™π‘Ž ∧ 0 𝑙𝑏) β†’ 0 𝑙(π‘Ž Β· 𝑏))))
16 fvexd 6907 . . . . . 6 (π‘Ÿ = 𝑅 β†’ (Baseβ€˜π‘Ÿ) ∈ V)
17 simpr 486 . . . . . . . . . . 11 ((π‘Ÿ = 𝑅 ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ 𝑣 = (Baseβ€˜π‘Ÿ))
18 fveq2 6892 . . . . . . . . . . . . 13 (π‘Ÿ = 𝑅 β†’ (Baseβ€˜π‘Ÿ) = (Baseβ€˜π‘…))
19 isorng.0 . . . . . . . . . . . . 13 𝐡 = (Baseβ€˜π‘…)
2018, 19eqtr4di 2791 . . . . . . . . . . . 12 (π‘Ÿ = 𝑅 β†’ (Baseβ€˜π‘Ÿ) = 𝐡)
2120adantr 482 . . . . . . . . . . 11 ((π‘Ÿ = 𝑅 ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ (Baseβ€˜π‘Ÿ) = 𝐡)
2217, 21eqtrd 2773 . . . . . . . . . 10 ((π‘Ÿ = 𝑅 ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ 𝑣 = 𝐡)
23 raleq 3323 . . . . . . . . . . 11 (𝑣 = 𝐡 β†’ (βˆ€π‘ ∈ 𝑣 ((π‘§π‘™π‘Ž ∧ 𝑧𝑙𝑏) β†’ 𝑧𝑙(π‘Žπ‘‘π‘)) ↔ βˆ€π‘ ∈ 𝐡 ((π‘§π‘™π‘Ž ∧ 𝑧𝑙𝑏) β†’ 𝑧𝑙(π‘Žπ‘‘π‘))))
2423raleqbi1dv 3334 . . . . . . . . . 10 (𝑣 = 𝐡 β†’ (βˆ€π‘Ž ∈ 𝑣 βˆ€π‘ ∈ 𝑣 ((π‘§π‘™π‘Ž ∧ 𝑧𝑙𝑏) β†’ 𝑧𝑙(π‘Žπ‘‘π‘)) ↔ βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 ((π‘§π‘™π‘Ž ∧ 𝑧𝑙𝑏) β†’ 𝑧𝑙(π‘Žπ‘‘π‘))))
2522, 24syl 17 . . . . . . . . 9 ((π‘Ÿ = 𝑅 ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ (βˆ€π‘Ž ∈ 𝑣 βˆ€π‘ ∈ 𝑣 ((π‘§π‘™π‘Ž ∧ 𝑧𝑙𝑏) β†’ 𝑧𝑙(π‘Žπ‘‘π‘)) ↔ βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 ((π‘§π‘™π‘Ž ∧ 𝑧𝑙𝑏) β†’ 𝑧𝑙(π‘Žπ‘‘π‘))))
2625sbcbidv 3837 . . . . . . . 8 ((π‘Ÿ = 𝑅 ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ ([(leβ€˜π‘Ÿ) / 𝑙]βˆ€π‘Ž ∈ 𝑣 βˆ€π‘ ∈ 𝑣 ((π‘§π‘™π‘Ž ∧ 𝑧𝑙𝑏) β†’ 𝑧𝑙(π‘Žπ‘‘π‘)) ↔ [(leβ€˜π‘Ÿ) / 𝑙]βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 ((π‘§π‘™π‘Ž ∧ 𝑧𝑙𝑏) β†’ 𝑧𝑙(π‘Žπ‘‘π‘))))
2726sbcbidv 3837 . . . . . . 7 ((π‘Ÿ = 𝑅 ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ ([(.rβ€˜π‘Ÿ) / 𝑑][(leβ€˜π‘Ÿ) / 𝑙]βˆ€π‘Ž ∈ 𝑣 βˆ€π‘ ∈ 𝑣 ((π‘§π‘™π‘Ž ∧ 𝑧𝑙𝑏) β†’ 𝑧𝑙(π‘Žπ‘‘π‘)) ↔ [(.rβ€˜π‘Ÿ) / 𝑑][(leβ€˜π‘Ÿ) / 𝑙]βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 ((π‘§π‘™π‘Ž ∧ 𝑧𝑙𝑏) β†’ 𝑧𝑙(π‘Žπ‘‘π‘))))
2827sbcbidv 3837 . . . . . 6 ((π‘Ÿ = 𝑅 ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ ([(0gβ€˜π‘Ÿ) / 𝑧][(.rβ€˜π‘Ÿ) / 𝑑][(leβ€˜π‘Ÿ) / 𝑙]βˆ€π‘Ž ∈ 𝑣 βˆ€π‘ ∈ 𝑣 ((π‘§π‘™π‘Ž ∧ 𝑧𝑙𝑏) β†’ 𝑧𝑙(π‘Žπ‘‘π‘)) ↔ [(0gβ€˜π‘Ÿ) / 𝑧][(.rβ€˜π‘Ÿ) / 𝑑][(leβ€˜π‘Ÿ) / 𝑙]βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 ((π‘§π‘™π‘Ž ∧ 𝑧𝑙𝑏) β†’ 𝑧𝑙(π‘Žπ‘‘π‘))))
2916, 28sbcied 3823 . . . . 5 (π‘Ÿ = 𝑅 β†’ ([(Baseβ€˜π‘Ÿ) / 𝑣][(0gβ€˜π‘Ÿ) / 𝑧][(.rβ€˜π‘Ÿ) / 𝑑][(leβ€˜π‘Ÿ) / 𝑙]βˆ€π‘Ž ∈ 𝑣 βˆ€π‘ ∈ 𝑣 ((π‘§π‘™π‘Ž ∧ 𝑧𝑙𝑏) β†’ 𝑧𝑙(π‘Žπ‘‘π‘)) ↔ [(0gβ€˜π‘Ÿ) / 𝑧][(.rβ€˜π‘Ÿ) / 𝑑][(leβ€˜π‘Ÿ) / 𝑙]βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 ((π‘§π‘™π‘Ž ∧ 𝑧𝑙𝑏) β†’ 𝑧𝑙(π‘Žπ‘‘π‘))))
30 fvexd 6907 . . . . . 6 (π‘Ÿ = 𝑅 β†’ (0gβ€˜π‘Ÿ) ∈ V)
31 simpr 486 . . . . . . . . . . . . 13 ((π‘Ÿ = 𝑅 ∧ 𝑧 = (0gβ€˜π‘Ÿ)) β†’ 𝑧 = (0gβ€˜π‘Ÿ))
32 fveq2 6892 . . . . . . . . . . . . . . 15 (π‘Ÿ = 𝑅 β†’ (0gβ€˜π‘Ÿ) = (0gβ€˜π‘…))
33 isorng.1 . . . . . . . . . . . . . . 15 0 = (0gβ€˜π‘…)
3432, 33eqtr4di 2791 . . . . . . . . . . . . . 14 (π‘Ÿ = 𝑅 β†’ (0gβ€˜π‘Ÿ) = 0 )
3534adantr 482 . . . . . . . . . . . . 13 ((π‘Ÿ = 𝑅 ∧ 𝑧 = (0gβ€˜π‘Ÿ)) β†’ (0gβ€˜π‘Ÿ) = 0 )
3631, 35eqtrd 2773 . . . . . . . . . . . 12 ((π‘Ÿ = 𝑅 ∧ 𝑧 = (0gβ€˜π‘Ÿ)) β†’ 𝑧 = 0 )
3736breq1d 5159 . . . . . . . . . . 11 ((π‘Ÿ = 𝑅 ∧ 𝑧 = (0gβ€˜π‘Ÿ)) β†’ (π‘§π‘™π‘Ž ↔ 0 π‘™π‘Ž))
3836breq1d 5159 . . . . . . . . . . 11 ((π‘Ÿ = 𝑅 ∧ 𝑧 = (0gβ€˜π‘Ÿ)) β†’ (𝑧𝑙𝑏 ↔ 0 𝑙𝑏))
3937, 38anbi12d 632 . . . . . . . . . 10 ((π‘Ÿ = 𝑅 ∧ 𝑧 = (0gβ€˜π‘Ÿ)) β†’ ((π‘§π‘™π‘Ž ∧ 𝑧𝑙𝑏) ↔ ( 0 π‘™π‘Ž ∧ 0 𝑙𝑏)))
4036breq1d 5159 . . . . . . . . . 10 ((π‘Ÿ = 𝑅 ∧ 𝑧 = (0gβ€˜π‘Ÿ)) β†’ (𝑧𝑙(π‘Žπ‘‘π‘) ↔ 0 𝑙(π‘Žπ‘‘π‘)))
4139, 40imbi12d 345 . . . . . . . . 9 ((π‘Ÿ = 𝑅 ∧ 𝑧 = (0gβ€˜π‘Ÿ)) β†’ (((π‘§π‘™π‘Ž ∧ 𝑧𝑙𝑏) β†’ 𝑧𝑙(π‘Žπ‘‘π‘)) ↔ (( 0 π‘™π‘Ž ∧ 0 𝑙𝑏) β†’ 0 𝑙(π‘Žπ‘‘π‘))))
42412ralbidv 3219 . . . . . . . 8 ((π‘Ÿ = 𝑅 ∧ 𝑧 = (0gβ€˜π‘Ÿ)) β†’ (βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 ((π‘§π‘™π‘Ž ∧ 𝑧𝑙𝑏) β†’ 𝑧𝑙(π‘Žπ‘‘π‘)) ↔ βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 (( 0 π‘™π‘Ž ∧ 0 𝑙𝑏) β†’ 0 𝑙(π‘Žπ‘‘π‘))))
4342sbcbidv 3837 . . . . . . 7 ((π‘Ÿ = 𝑅 ∧ 𝑧 = (0gβ€˜π‘Ÿ)) β†’ ([(leβ€˜π‘Ÿ) / 𝑙]βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 ((π‘§π‘™π‘Ž ∧ 𝑧𝑙𝑏) β†’ 𝑧𝑙(π‘Žπ‘‘π‘)) ↔ [(leβ€˜π‘Ÿ) / 𝑙]βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 (( 0 π‘™π‘Ž ∧ 0 𝑙𝑏) β†’ 0 𝑙(π‘Žπ‘‘π‘))))
4443sbcbidv 3837 . . . . . 6 ((π‘Ÿ = 𝑅 ∧ 𝑧 = (0gβ€˜π‘Ÿ)) β†’ ([(.rβ€˜π‘Ÿ) / 𝑑][(leβ€˜π‘Ÿ) / 𝑙]βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 ((π‘§π‘™π‘Ž ∧ 𝑧𝑙𝑏) β†’ 𝑧𝑙(π‘Žπ‘‘π‘)) ↔ [(.rβ€˜π‘Ÿ) / 𝑑][(leβ€˜π‘Ÿ) / 𝑙]βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 (( 0 π‘™π‘Ž ∧ 0 𝑙𝑏) β†’ 0 𝑙(π‘Žπ‘‘π‘))))
4530, 44sbcied 3823 . . . . 5 (π‘Ÿ = 𝑅 β†’ ([(0gβ€˜π‘Ÿ) / 𝑧][(.rβ€˜π‘Ÿ) / 𝑑][(leβ€˜π‘Ÿ) / 𝑙]βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 ((π‘§π‘™π‘Ž ∧ 𝑧𝑙𝑏) β†’ 𝑧𝑙(π‘Žπ‘‘π‘)) ↔ [(.rβ€˜π‘Ÿ) / 𝑑][(leβ€˜π‘Ÿ) / 𝑙]βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 (( 0 π‘™π‘Ž ∧ 0 𝑙𝑏) β†’ 0 𝑙(π‘Žπ‘‘π‘))))
4629, 45bitr2d 280 . . . 4 (π‘Ÿ = 𝑅 β†’ ([(.rβ€˜π‘Ÿ) / 𝑑][(leβ€˜π‘Ÿ) / 𝑙]βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 (( 0 π‘™π‘Ž ∧ 0 𝑙𝑏) β†’ 0 𝑙(π‘Žπ‘‘π‘)) ↔ [(Baseβ€˜π‘Ÿ) / 𝑣][(0gβ€˜π‘Ÿ) / 𝑧][(.rβ€˜π‘Ÿ) / 𝑑][(leβ€˜π‘Ÿ) / 𝑙]βˆ€π‘Ž ∈ 𝑣 βˆ€π‘ ∈ 𝑣 ((π‘§π‘™π‘Ž ∧ 𝑧𝑙𝑏) β†’ 𝑧𝑙(π‘Žπ‘‘π‘))))
47 fvexd 6907 . . . . 5 (π‘Ÿ = 𝑅 β†’ (leβ€˜π‘Ÿ) ∈ V)
48 simpr 486 . . . . . . . . . 10 ((π‘Ÿ = 𝑅 ∧ 𝑙 = (leβ€˜π‘Ÿ)) β†’ 𝑙 = (leβ€˜π‘Ÿ))
49 simpl 484 . . . . . . . . . . . 12 ((π‘Ÿ = 𝑅 ∧ 𝑙 = (leβ€˜π‘Ÿ)) β†’ π‘Ÿ = 𝑅)
5049fveq2d 6896 . . . . . . . . . . 11 ((π‘Ÿ = 𝑅 ∧ 𝑙 = (leβ€˜π‘Ÿ)) β†’ (leβ€˜π‘Ÿ) = (leβ€˜π‘…))
51 isorng.3 . . . . . . . . . . 11 ≀ = (leβ€˜π‘…)
5250, 51eqtr4di 2791 . . . . . . . . . 10 ((π‘Ÿ = 𝑅 ∧ 𝑙 = (leβ€˜π‘Ÿ)) β†’ (leβ€˜π‘Ÿ) = ≀ )
5348, 52eqtrd 2773 . . . . . . . . 9 ((π‘Ÿ = 𝑅 ∧ 𝑙 = (leβ€˜π‘Ÿ)) β†’ 𝑙 = ≀ )
5453breqd 5160 . . . . . . . 8 ((π‘Ÿ = 𝑅 ∧ 𝑙 = (leβ€˜π‘Ÿ)) β†’ ( 0 π‘™π‘Ž ↔ 0 ≀ π‘Ž))
5553breqd 5160 . . . . . . . 8 ((π‘Ÿ = 𝑅 ∧ 𝑙 = (leβ€˜π‘Ÿ)) β†’ ( 0 𝑙𝑏 ↔ 0 ≀ 𝑏))
5654, 55anbi12d 632 . . . . . . 7 ((π‘Ÿ = 𝑅 ∧ 𝑙 = (leβ€˜π‘Ÿ)) β†’ (( 0 π‘™π‘Ž ∧ 0 𝑙𝑏) ↔ ( 0 ≀ π‘Ž ∧ 0 ≀ 𝑏)))
5753breqd 5160 . . . . . . 7 ((π‘Ÿ = 𝑅 ∧ 𝑙 = (leβ€˜π‘Ÿ)) β†’ ( 0 𝑙(π‘Ž Β· 𝑏) ↔ 0 ≀ (π‘Ž Β· 𝑏)))
5856, 57imbi12d 345 . . . . . 6 ((π‘Ÿ = 𝑅 ∧ 𝑙 = (leβ€˜π‘Ÿ)) β†’ ((( 0 π‘™π‘Ž ∧ 0 𝑙𝑏) β†’ 0 𝑙(π‘Ž Β· 𝑏)) ↔ (( 0 ≀ π‘Ž ∧ 0 ≀ 𝑏) β†’ 0 ≀ (π‘Ž Β· 𝑏))))
59582ralbidv 3219 . . . . 5 ((π‘Ÿ = 𝑅 ∧ 𝑙 = (leβ€˜π‘Ÿ)) β†’ (βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 (( 0 π‘™π‘Ž ∧ 0 𝑙𝑏) β†’ 0 𝑙(π‘Ž Β· 𝑏)) ↔ βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 (( 0 ≀ π‘Ž ∧ 0 ≀ 𝑏) β†’ 0 ≀ (π‘Ž Β· 𝑏))))
6047, 59sbcied 3823 . . . 4 (π‘Ÿ = 𝑅 β†’ ([(leβ€˜π‘Ÿ) / 𝑙]βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 (( 0 π‘™π‘Ž ∧ 0 𝑙𝑏) β†’ 0 𝑙(π‘Ž Β· 𝑏)) ↔ βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 (( 0 ≀ π‘Ž ∧ 0 ≀ 𝑏) β†’ 0 ≀ (π‘Ž Β· 𝑏))))
6115, 46, 603bitr3d 309 . . 3 (π‘Ÿ = 𝑅 β†’ ([(Baseβ€˜π‘Ÿ) / 𝑣][(0gβ€˜π‘Ÿ) / 𝑧][(.rβ€˜π‘Ÿ) / 𝑑][(leβ€˜π‘Ÿ) / 𝑙]βˆ€π‘Ž ∈ 𝑣 βˆ€π‘ ∈ 𝑣 ((π‘§π‘™π‘Ž ∧ 𝑧𝑙𝑏) β†’ 𝑧𝑙(π‘Žπ‘‘π‘)) ↔ βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 (( 0 ≀ π‘Ž ∧ 0 ≀ 𝑏) β†’ 0 ≀ (π‘Ž Β· 𝑏))))
62 df-orng 32415 . . 3 oRing = {π‘Ÿ ∈ (Ring ∩ oGrp) ∣ [(Baseβ€˜π‘Ÿ) / 𝑣][(0gβ€˜π‘Ÿ) / 𝑧][(.rβ€˜π‘Ÿ) / 𝑑][(leβ€˜π‘Ÿ) / 𝑙]βˆ€π‘Ž ∈ 𝑣 βˆ€π‘ ∈ 𝑣 ((π‘§π‘™π‘Ž ∧ 𝑧𝑙𝑏) β†’ 𝑧𝑙(π‘Žπ‘‘π‘))}
6361, 62elrab2 3687 . 2 (𝑅 ∈ oRing ↔ (𝑅 ∈ (Ring ∩ oGrp) ∧ βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 (( 0 ≀ π‘Ž ∧ 0 ≀ 𝑏) β†’ 0 ≀ (π‘Ž Β· 𝑏))))
64 df-3an 1090 . 2 ((𝑅 ∈ Ring ∧ 𝑅 ∈ oGrp ∧ βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 (( 0 ≀ π‘Ž ∧ 0 ≀ 𝑏) β†’ 0 ≀ (π‘Ž Β· 𝑏))) ↔ ((𝑅 ∈ Ring ∧ 𝑅 ∈ oGrp) ∧ βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 (( 0 ≀ π‘Ž ∧ 0 ≀ 𝑏) β†’ 0 ≀ (π‘Ž Β· 𝑏))))
652, 63, 643bitr4i 303 1 (𝑅 ∈ oRing ↔ (𝑅 ∈ Ring ∧ 𝑅 ∈ oGrp ∧ βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 (( 0 ≀ π‘Ž ∧ 0 ≀ 𝑏) β†’ 0 ≀ (π‘Ž Β· 𝑏))))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 397   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107  βˆ€wral 3062  Vcvv 3475  [wsbc 3778   ∩ cin 3948   class class class wbr 5149  β€˜cfv 6544  (class class class)co 7409  Basecbs 17144  .rcmulr 17198  lecple 17204  0gc0g 17385  Ringcrg 20056  oGrpcogrp 32216  oRingcorng 32413
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-nul 5307
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ne 2942  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-sbc 3779  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-iota 6496  df-fv 6552  df-ov 7412  df-orng 32415
This theorem is referenced by:  orngring  32418  orngogrp  32419  orngmul  32421  suborng  32433  reofld  32459
  Copyright terms: Public domain W3C validator