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 32954
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 3960 . . 3 (𝑅 ∈ (Ring ∩ oGrp) ↔ (𝑅 ∈ Ring ∧ 𝑅 ∈ oGrp))
21anbi1i 623 . 2 ((𝑅 ∈ (Ring ∩ oGrp) ∧ βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 (( 0 ≀ π‘Ž ∧ 0 ≀ 𝑏) β†’ 0 ≀ (π‘Ž Β· 𝑏))) ↔ ((𝑅 ∈ Ring ∧ 𝑅 ∈ oGrp) ∧ βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 (( 0 ≀ π‘Ž ∧ 0 ≀ 𝑏) β†’ 0 ≀ (π‘Ž Β· 𝑏))))
3 fvexd 6906 . . . . 5 (π‘Ÿ = 𝑅 β†’ (.rβ€˜π‘Ÿ) ∈ V)
4 simpr 484 . . . . . . . . . . 11 ((π‘Ÿ = 𝑅 ∧ 𝑑 = (.rβ€˜π‘Ÿ)) β†’ 𝑑 = (.rβ€˜π‘Ÿ))
5 simpl 482 . . . . . . . . . . . . 13 ((π‘Ÿ = 𝑅 ∧ 𝑑 = (.rβ€˜π‘Ÿ)) β†’ π‘Ÿ = 𝑅)
65fveq2d 6895 . . . . . . . . . . . 12 ((π‘Ÿ = 𝑅 ∧ 𝑑 = (.rβ€˜π‘Ÿ)) β†’ (.rβ€˜π‘Ÿ) = (.rβ€˜π‘…))
7 isorng.2 . . . . . . . . . . . 12 Β· = (.rβ€˜π‘…)
86, 7eqtr4di 2785 . . . . . . . . . . 11 ((π‘Ÿ = 𝑅 ∧ 𝑑 = (.rβ€˜π‘Ÿ)) β†’ (.rβ€˜π‘Ÿ) = Β· )
94, 8eqtrd 2767 . . . . . . . . . 10 ((π‘Ÿ = 𝑅 ∧ 𝑑 = (.rβ€˜π‘Ÿ)) β†’ 𝑑 = Β· )
109oveqd 7431 . . . . . . . . 9 ((π‘Ÿ = 𝑅 ∧ 𝑑 = (.rβ€˜π‘Ÿ)) β†’ (π‘Žπ‘‘π‘) = (π‘Ž Β· 𝑏))
1110breq2d 5154 . . . . . . . 8 ((π‘Ÿ = 𝑅 ∧ 𝑑 = (.rβ€˜π‘Ÿ)) β†’ ( 0 𝑙(π‘Žπ‘‘π‘) ↔ 0 𝑙(π‘Ž Β· 𝑏)))
1211imbi2d 340 . . . . . . 7 ((π‘Ÿ = 𝑅 ∧ 𝑑 = (.rβ€˜π‘Ÿ)) β†’ ((( 0 π‘™π‘Ž ∧ 0 𝑙𝑏) β†’ 0 𝑙(π‘Žπ‘‘π‘)) ↔ (( 0 π‘™π‘Ž ∧ 0 𝑙𝑏) β†’ 0 𝑙(π‘Ž Β· 𝑏))))
13122ralbidv 3213 . . . . . 6 ((π‘Ÿ = 𝑅 ∧ 𝑑 = (.rβ€˜π‘Ÿ)) β†’ (βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 (( 0 π‘™π‘Ž ∧ 0 𝑙𝑏) β†’ 0 𝑙(π‘Žπ‘‘π‘)) ↔ βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 (( 0 π‘™π‘Ž ∧ 0 𝑙𝑏) β†’ 0 𝑙(π‘Ž Β· 𝑏))))
1413sbcbidv 3833 . . . . 5 ((π‘Ÿ = 𝑅 ∧ 𝑑 = (.rβ€˜π‘Ÿ)) β†’ ([(leβ€˜π‘Ÿ) / 𝑙]βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 (( 0 π‘™π‘Ž ∧ 0 𝑙𝑏) β†’ 0 𝑙(π‘Žπ‘‘π‘)) ↔ [(leβ€˜π‘Ÿ) / 𝑙]βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 (( 0 π‘™π‘Ž ∧ 0 𝑙𝑏) β†’ 0 𝑙(π‘Ž Β· 𝑏))))
153, 14sbcied 3819 . . . 4 (π‘Ÿ = 𝑅 β†’ ([(.rβ€˜π‘Ÿ) / 𝑑][(leβ€˜π‘Ÿ) / 𝑙]βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 (( 0 π‘™π‘Ž ∧ 0 𝑙𝑏) β†’ 0 𝑙(π‘Žπ‘‘π‘)) ↔ [(leβ€˜π‘Ÿ) / 𝑙]βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 (( 0 π‘™π‘Ž ∧ 0 𝑙𝑏) β†’ 0 𝑙(π‘Ž Β· 𝑏))))
16 fvexd 6906 . . . . . 6 (π‘Ÿ = 𝑅 β†’ (Baseβ€˜π‘Ÿ) ∈ V)
17 simpr 484 . . . . . . . . . . 11 ((π‘Ÿ = 𝑅 ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ 𝑣 = (Baseβ€˜π‘Ÿ))
18 fveq2 6891 . . . . . . . . . . . . 13 (π‘Ÿ = 𝑅 β†’ (Baseβ€˜π‘Ÿ) = (Baseβ€˜π‘…))
19 isorng.0 . . . . . . . . . . . . 13 𝐡 = (Baseβ€˜π‘…)
2018, 19eqtr4di 2785 . . . . . . . . . . . 12 (π‘Ÿ = 𝑅 β†’ (Baseβ€˜π‘Ÿ) = 𝐡)
2120adantr 480 . . . . . . . . . . 11 ((π‘Ÿ = 𝑅 ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ (Baseβ€˜π‘Ÿ) = 𝐡)
2217, 21eqtrd 2767 . . . . . . . . . 10 ((π‘Ÿ = 𝑅 ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ 𝑣 = 𝐡)
23 raleq 3317 . . . . . . . . . . 11 (𝑣 = 𝐡 β†’ (βˆ€π‘ ∈ 𝑣 ((π‘§π‘™π‘Ž ∧ 𝑧𝑙𝑏) β†’ 𝑧𝑙(π‘Žπ‘‘π‘)) ↔ βˆ€π‘ ∈ 𝐡 ((π‘§π‘™π‘Ž ∧ 𝑧𝑙𝑏) β†’ 𝑧𝑙(π‘Žπ‘‘π‘))))
2423raleqbi1dv 3328 . . . . . . . . . 10 (𝑣 = 𝐡 β†’ (βˆ€π‘Ž ∈ 𝑣 βˆ€π‘ ∈ 𝑣 ((π‘§π‘™π‘Ž ∧ 𝑧𝑙𝑏) β†’ 𝑧𝑙(π‘Žπ‘‘π‘)) ↔ βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 ((π‘§π‘™π‘Ž ∧ 𝑧𝑙𝑏) β†’ 𝑧𝑙(π‘Žπ‘‘π‘))))
2522, 24syl 17 . . . . . . . . 9 ((π‘Ÿ = 𝑅 ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ (βˆ€π‘Ž ∈ 𝑣 βˆ€π‘ ∈ 𝑣 ((π‘§π‘™π‘Ž ∧ 𝑧𝑙𝑏) β†’ 𝑧𝑙(π‘Žπ‘‘π‘)) ↔ βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 ((π‘§π‘™π‘Ž ∧ 𝑧𝑙𝑏) β†’ 𝑧𝑙(π‘Žπ‘‘π‘))))
2625sbcbidv 3833 . . . . . . . 8 ((π‘Ÿ = 𝑅 ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ ([(leβ€˜π‘Ÿ) / 𝑙]βˆ€π‘Ž ∈ 𝑣 βˆ€π‘ ∈ 𝑣 ((π‘§π‘™π‘Ž ∧ 𝑧𝑙𝑏) β†’ 𝑧𝑙(π‘Žπ‘‘π‘)) ↔ [(leβ€˜π‘Ÿ) / 𝑙]βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 ((π‘§π‘™π‘Ž ∧ 𝑧𝑙𝑏) β†’ 𝑧𝑙(π‘Žπ‘‘π‘))))
2726sbcbidv 3833 . . . . . . 7 ((π‘Ÿ = 𝑅 ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ ([(.rβ€˜π‘Ÿ) / 𝑑][(leβ€˜π‘Ÿ) / 𝑙]βˆ€π‘Ž ∈ 𝑣 βˆ€π‘ ∈ 𝑣 ((π‘§π‘™π‘Ž ∧ 𝑧𝑙𝑏) β†’ 𝑧𝑙(π‘Žπ‘‘π‘)) ↔ [(.rβ€˜π‘Ÿ) / 𝑑][(leβ€˜π‘Ÿ) / 𝑙]βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 ((π‘§π‘™π‘Ž ∧ 𝑧𝑙𝑏) β†’ 𝑧𝑙(π‘Žπ‘‘π‘))))
2827sbcbidv 3833 . . . . . 6 ((π‘Ÿ = 𝑅 ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ ([(0gβ€˜π‘Ÿ) / 𝑧][(.rβ€˜π‘Ÿ) / 𝑑][(leβ€˜π‘Ÿ) / 𝑙]βˆ€π‘Ž ∈ 𝑣 βˆ€π‘ ∈ 𝑣 ((π‘§π‘™π‘Ž ∧ 𝑧𝑙𝑏) β†’ 𝑧𝑙(π‘Žπ‘‘π‘)) ↔ [(0gβ€˜π‘Ÿ) / 𝑧][(.rβ€˜π‘Ÿ) / 𝑑][(leβ€˜π‘Ÿ) / 𝑙]βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 ((π‘§π‘™π‘Ž ∧ 𝑧𝑙𝑏) β†’ 𝑧𝑙(π‘Žπ‘‘π‘))))
2916, 28sbcied 3819 . . . . 5 (π‘Ÿ = 𝑅 β†’ ([(Baseβ€˜π‘Ÿ) / 𝑣][(0gβ€˜π‘Ÿ) / 𝑧][(.rβ€˜π‘Ÿ) / 𝑑][(leβ€˜π‘Ÿ) / 𝑙]βˆ€π‘Ž ∈ 𝑣 βˆ€π‘ ∈ 𝑣 ((π‘§π‘™π‘Ž ∧ 𝑧𝑙𝑏) β†’ 𝑧𝑙(π‘Žπ‘‘π‘)) ↔ [(0gβ€˜π‘Ÿ) / 𝑧][(.rβ€˜π‘Ÿ) / 𝑑][(leβ€˜π‘Ÿ) / 𝑙]βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 ((π‘§π‘™π‘Ž ∧ 𝑧𝑙𝑏) β†’ 𝑧𝑙(π‘Žπ‘‘π‘))))
30 fvexd 6906 . . . . . 6 (π‘Ÿ = 𝑅 β†’ (0gβ€˜π‘Ÿ) ∈ V)
31 simpr 484 . . . . . . . . . . . . 13 ((π‘Ÿ = 𝑅 ∧ 𝑧 = (0gβ€˜π‘Ÿ)) β†’ 𝑧 = (0gβ€˜π‘Ÿ))
32 fveq2 6891 . . . . . . . . . . . . . . 15 (π‘Ÿ = 𝑅 β†’ (0gβ€˜π‘Ÿ) = (0gβ€˜π‘…))
33 isorng.1 . . . . . . . . . . . . . . 15 0 = (0gβ€˜π‘…)
3432, 33eqtr4di 2785 . . . . . . . . . . . . . 14 (π‘Ÿ = 𝑅 β†’ (0gβ€˜π‘Ÿ) = 0 )
3534adantr 480 . . . . . . . . . . . . 13 ((π‘Ÿ = 𝑅 ∧ 𝑧 = (0gβ€˜π‘Ÿ)) β†’ (0gβ€˜π‘Ÿ) = 0 )
3631, 35eqtrd 2767 . . . . . . . . . . . 12 ((π‘Ÿ = 𝑅 ∧ 𝑧 = (0gβ€˜π‘Ÿ)) β†’ 𝑧 = 0 )
3736breq1d 5152 . . . . . . . . . . 11 ((π‘Ÿ = 𝑅 ∧ 𝑧 = (0gβ€˜π‘Ÿ)) β†’ (π‘§π‘™π‘Ž ↔ 0 π‘™π‘Ž))
3836breq1d 5152 . . . . . . . . . . 11 ((π‘Ÿ = 𝑅 ∧ 𝑧 = (0gβ€˜π‘Ÿ)) β†’ (𝑧𝑙𝑏 ↔ 0 𝑙𝑏))
3937, 38anbi12d 630 . . . . . . . . . 10 ((π‘Ÿ = 𝑅 ∧ 𝑧 = (0gβ€˜π‘Ÿ)) β†’ ((π‘§π‘™π‘Ž ∧ 𝑧𝑙𝑏) ↔ ( 0 π‘™π‘Ž ∧ 0 𝑙𝑏)))
4036breq1d 5152 . . . . . . . . . 10 ((π‘Ÿ = 𝑅 ∧ 𝑧 = (0gβ€˜π‘Ÿ)) β†’ (𝑧𝑙(π‘Žπ‘‘π‘) ↔ 0 𝑙(π‘Žπ‘‘π‘)))
4139, 40imbi12d 344 . . . . . . . . 9 ((π‘Ÿ = 𝑅 ∧ 𝑧 = (0gβ€˜π‘Ÿ)) β†’ (((π‘§π‘™π‘Ž ∧ 𝑧𝑙𝑏) β†’ 𝑧𝑙(π‘Žπ‘‘π‘)) ↔ (( 0 π‘™π‘Ž ∧ 0 𝑙𝑏) β†’ 0 𝑙(π‘Žπ‘‘π‘))))
42412ralbidv 3213 . . . . . . . 8 ((π‘Ÿ = 𝑅 ∧ 𝑧 = (0gβ€˜π‘Ÿ)) β†’ (βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 ((π‘§π‘™π‘Ž ∧ 𝑧𝑙𝑏) β†’ 𝑧𝑙(π‘Žπ‘‘π‘)) ↔ βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 (( 0 π‘™π‘Ž ∧ 0 𝑙𝑏) β†’ 0 𝑙(π‘Žπ‘‘π‘))))
4342sbcbidv 3833 . . . . . . 7 ((π‘Ÿ = 𝑅 ∧ 𝑧 = (0gβ€˜π‘Ÿ)) β†’ ([(leβ€˜π‘Ÿ) / 𝑙]βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 ((π‘§π‘™π‘Ž ∧ 𝑧𝑙𝑏) β†’ 𝑧𝑙(π‘Žπ‘‘π‘)) ↔ [(leβ€˜π‘Ÿ) / 𝑙]βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 (( 0 π‘™π‘Ž ∧ 0 𝑙𝑏) β†’ 0 𝑙(π‘Žπ‘‘π‘))))
4443sbcbidv 3833 . . . . . 6 ((π‘Ÿ = 𝑅 ∧ 𝑧 = (0gβ€˜π‘Ÿ)) β†’ ([(.rβ€˜π‘Ÿ) / 𝑑][(leβ€˜π‘Ÿ) / 𝑙]βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 ((π‘§π‘™π‘Ž ∧ 𝑧𝑙𝑏) β†’ 𝑧𝑙(π‘Žπ‘‘π‘)) ↔ [(.rβ€˜π‘Ÿ) / 𝑑][(leβ€˜π‘Ÿ) / 𝑙]βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 (( 0 π‘™π‘Ž ∧ 0 𝑙𝑏) β†’ 0 𝑙(π‘Žπ‘‘π‘))))
4530, 44sbcied 3819 . . . . 5 (π‘Ÿ = 𝑅 β†’ ([(0gβ€˜π‘Ÿ) / 𝑧][(.rβ€˜π‘Ÿ) / 𝑑][(leβ€˜π‘Ÿ) / 𝑙]βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 ((π‘§π‘™π‘Ž ∧ 𝑧𝑙𝑏) β†’ 𝑧𝑙(π‘Žπ‘‘π‘)) ↔ [(.rβ€˜π‘Ÿ) / 𝑑][(leβ€˜π‘Ÿ) / 𝑙]βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 (( 0 π‘™π‘Ž ∧ 0 𝑙𝑏) β†’ 0 𝑙(π‘Žπ‘‘π‘))))
4629, 45bitr2d 280 . . . 4 (π‘Ÿ = 𝑅 β†’ ([(.rβ€˜π‘Ÿ) / 𝑑][(leβ€˜π‘Ÿ) / 𝑙]βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 (( 0 π‘™π‘Ž ∧ 0 𝑙𝑏) β†’ 0 𝑙(π‘Žπ‘‘π‘)) ↔ [(Baseβ€˜π‘Ÿ) / 𝑣][(0gβ€˜π‘Ÿ) / 𝑧][(.rβ€˜π‘Ÿ) / 𝑑][(leβ€˜π‘Ÿ) / 𝑙]βˆ€π‘Ž ∈ 𝑣 βˆ€π‘ ∈ 𝑣 ((π‘§π‘™π‘Ž ∧ 𝑧𝑙𝑏) β†’ 𝑧𝑙(π‘Žπ‘‘π‘))))
47 fvexd 6906 . . . . 5 (π‘Ÿ = 𝑅 β†’ (leβ€˜π‘Ÿ) ∈ V)
48 simpr 484 . . . . . . . . . 10 ((π‘Ÿ = 𝑅 ∧ 𝑙 = (leβ€˜π‘Ÿ)) β†’ 𝑙 = (leβ€˜π‘Ÿ))
49 simpl 482 . . . . . . . . . . . 12 ((π‘Ÿ = 𝑅 ∧ 𝑙 = (leβ€˜π‘Ÿ)) β†’ π‘Ÿ = 𝑅)
5049fveq2d 6895 . . . . . . . . . . 11 ((π‘Ÿ = 𝑅 ∧ 𝑙 = (leβ€˜π‘Ÿ)) β†’ (leβ€˜π‘Ÿ) = (leβ€˜π‘…))
51 isorng.3 . . . . . . . . . . 11 ≀ = (leβ€˜π‘…)
5250, 51eqtr4di 2785 . . . . . . . . . 10 ((π‘Ÿ = 𝑅 ∧ 𝑙 = (leβ€˜π‘Ÿ)) β†’ (leβ€˜π‘Ÿ) = ≀ )
5348, 52eqtrd 2767 . . . . . . . . 9 ((π‘Ÿ = 𝑅 ∧ 𝑙 = (leβ€˜π‘Ÿ)) β†’ 𝑙 = ≀ )
5453breqd 5153 . . . . . . . 8 ((π‘Ÿ = 𝑅 ∧ 𝑙 = (leβ€˜π‘Ÿ)) β†’ ( 0 π‘™π‘Ž ↔ 0 ≀ π‘Ž))
5553breqd 5153 . . . . . . . 8 ((π‘Ÿ = 𝑅 ∧ 𝑙 = (leβ€˜π‘Ÿ)) β†’ ( 0 𝑙𝑏 ↔ 0 ≀ 𝑏))
5654, 55anbi12d 630 . . . . . . 7 ((π‘Ÿ = 𝑅 ∧ 𝑙 = (leβ€˜π‘Ÿ)) β†’ (( 0 π‘™π‘Ž ∧ 0 𝑙𝑏) ↔ ( 0 ≀ π‘Ž ∧ 0 ≀ 𝑏)))
5753breqd 5153 . . . . . . 7 ((π‘Ÿ = 𝑅 ∧ 𝑙 = (leβ€˜π‘Ÿ)) β†’ ( 0 𝑙(π‘Ž Β· 𝑏) ↔ 0 ≀ (π‘Ž Β· 𝑏)))
5856, 57imbi12d 344 . . . . . 6 ((π‘Ÿ = 𝑅 ∧ 𝑙 = (leβ€˜π‘Ÿ)) β†’ ((( 0 π‘™π‘Ž ∧ 0 𝑙𝑏) β†’ 0 𝑙(π‘Ž Β· 𝑏)) ↔ (( 0 ≀ π‘Ž ∧ 0 ≀ 𝑏) β†’ 0 ≀ (π‘Ž Β· 𝑏))))
59582ralbidv 3213 . . . . 5 ((π‘Ÿ = 𝑅 ∧ 𝑙 = (leβ€˜π‘Ÿ)) β†’ (βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 (( 0 π‘™π‘Ž ∧ 0 𝑙𝑏) β†’ 0 𝑙(π‘Ž Β· 𝑏)) ↔ βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 (( 0 ≀ π‘Ž ∧ 0 ≀ 𝑏) β†’ 0 ≀ (π‘Ž Β· 𝑏))))
6047, 59sbcied 3819 . . . 4 (π‘Ÿ = 𝑅 β†’ ([(leβ€˜π‘Ÿ) / 𝑙]βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 (( 0 π‘™π‘Ž ∧ 0 𝑙𝑏) β†’ 0 𝑙(π‘Ž Β· 𝑏)) ↔ βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 (( 0 ≀ π‘Ž ∧ 0 ≀ 𝑏) β†’ 0 ≀ (π‘Ž Β· 𝑏))))
6115, 46, 603bitr3d 309 . . 3 (π‘Ÿ = 𝑅 β†’ ([(Baseβ€˜π‘Ÿ) / 𝑣][(0gβ€˜π‘Ÿ) / 𝑧][(.rβ€˜π‘Ÿ) / 𝑑][(leβ€˜π‘Ÿ) / 𝑙]βˆ€π‘Ž ∈ 𝑣 βˆ€π‘ ∈ 𝑣 ((π‘§π‘™π‘Ž ∧ 𝑧𝑙𝑏) β†’ 𝑧𝑙(π‘Žπ‘‘π‘)) ↔ βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 (( 0 ≀ π‘Ž ∧ 0 ≀ 𝑏) β†’ 0 ≀ (π‘Ž Β· 𝑏))))
62 df-orng 32952 . . 3 oRing = {π‘Ÿ ∈ (Ring ∩ oGrp) ∣ [(Baseβ€˜π‘Ÿ) / 𝑣][(0gβ€˜π‘Ÿ) / 𝑧][(.rβ€˜π‘Ÿ) / 𝑑][(leβ€˜π‘Ÿ) / 𝑙]βˆ€π‘Ž ∈ 𝑣 βˆ€π‘ ∈ 𝑣 ((π‘§π‘™π‘Ž ∧ 𝑧𝑙𝑏) β†’ 𝑧𝑙(π‘Žπ‘‘π‘))}
6361, 62elrab2 3683 . 2 (𝑅 ∈ oRing ↔ (𝑅 ∈ (Ring ∩ oGrp) ∧ βˆ€π‘Ž ∈ 𝐡 βˆ€π‘ ∈ 𝐡 (( 0 ≀ π‘Ž ∧ 0 ≀ 𝑏) β†’ 0 ≀ (π‘Ž Β· 𝑏))))
64 df-3an 1087 . 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 395   ∧ w3a 1085   = wceq 1534   ∈ wcel 2099  βˆ€wral 3056  Vcvv 3469  [wsbc 3774   ∩ cin 3943   class class class wbr 5142  β€˜cfv 6542  (class class class)co 7414  Basecbs 17171  .rcmulr 17225  lecple 17231  0gc0g 17412  Ringcrg 20164  oGrpcogrp 32756  oRingcorng 32950
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2698  ax-nul 5300
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2705  df-cleq 2719  df-clel 2805  df-ne 2936  df-ral 3057  df-rex 3066  df-rab 3428  df-v 3471  df-sbc 3775  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4319  df-if 4525  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4904  df-br 5143  df-iota 6494  df-fv 6550  df-ov 7417  df-orng 32952
This theorem is referenced by:  orngring  32955  orngogrp  32956  orngmul  32958  suborng  32970  reofld  32996
  Copyright terms: Public domain W3C validator