Metamath Proof Explorer


Theorem isdrngo1

Description: The predicate "is a division ring". (Contributed by Jeff Madsen, 8-Jun-2010)

Ref Expression
Hypotheses isdivrng1.1 𝐺 = ( 1st𝑅 )
isdivrng1.2 𝐻 = ( 2nd𝑅 )
isdivrng1.3 𝑍 = ( GId ‘ 𝐺 )
isdivrng1.4 𝑋 = ran 𝐺
Assertion isdrngo1 ( 𝑅 ∈ DivRingOps ↔ ( 𝑅 ∈ RingOps ∧ ( 𝐻 ↾ ( ( 𝑋 ∖ { 𝑍 } ) × ( 𝑋 ∖ { 𝑍 } ) ) ) ∈ GrpOp ) )

Proof

Step Hyp Ref Expression
1 isdivrng1.1 𝐺 = ( 1st𝑅 )
2 isdivrng1.2 𝐻 = ( 2nd𝑅 )
3 isdivrng1.3 𝑍 = ( GId ‘ 𝐺 )
4 isdivrng1.4 𝑋 = ran 𝐺
5 df-drngo DivRingOps = { ⟨ 𝑔 , ⟩ ∣ ( ⟨ 𝑔 , ⟩ ∈ RingOps ∧ ( ↾ ( ( ran 𝑔 ∖ { ( GId ‘ 𝑔 ) } ) × ( ran 𝑔 ∖ { ( GId ‘ 𝑔 ) } ) ) ) ∈ GrpOp ) }
6 5 relopabiv Rel DivRingOps
7 1st2nd ( ( Rel DivRingOps ∧ 𝑅 ∈ DivRingOps ) → 𝑅 = ⟨ ( 1st𝑅 ) , ( 2nd𝑅 ) ⟩ )
8 6 7 mpan ( 𝑅 ∈ DivRingOps → 𝑅 = ⟨ ( 1st𝑅 ) , ( 2nd𝑅 ) ⟩ )
9 relrngo Rel RingOps
10 1st2nd ( ( Rel RingOps ∧ 𝑅 ∈ RingOps ) → 𝑅 = ⟨ ( 1st𝑅 ) , ( 2nd𝑅 ) ⟩ )
11 9 10 mpan ( 𝑅 ∈ RingOps → 𝑅 = ⟨ ( 1st𝑅 ) , ( 2nd𝑅 ) ⟩ )
12 11 adantr ( ( 𝑅 ∈ RingOps ∧ ( 𝐻 ↾ ( ( 𝑋 ∖ { 𝑍 } ) × ( 𝑋 ∖ { 𝑍 } ) ) ) ∈ GrpOp ) → 𝑅 = ⟨ ( 1st𝑅 ) , ( 2nd𝑅 ) ⟩ )
13 1 2 opeq12i 𝐺 , 𝐻 ⟩ = ⟨ ( 1st𝑅 ) , ( 2nd𝑅 ) ⟩
14 13 eqeq2i ( 𝑅 = ⟨ 𝐺 , 𝐻 ⟩ ↔ 𝑅 = ⟨ ( 1st𝑅 ) , ( 2nd𝑅 ) ⟩ )
15 2 fvexi 𝐻 ∈ V
16 isdivrngo ( 𝐻 ∈ V → ( ⟨ 𝐺 , 𝐻 ⟩ ∈ DivRingOps ↔ ( ⟨ 𝐺 , 𝐻 ⟩ ∈ RingOps ∧ ( 𝐻 ↾ ( ( ran 𝐺 ∖ { ( GId ‘ 𝐺 ) } ) × ( ran 𝐺 ∖ { ( GId ‘ 𝐺 ) } ) ) ) ∈ GrpOp ) ) )
17 15 16 ax-mp ( ⟨ 𝐺 , 𝐻 ⟩ ∈ DivRingOps ↔ ( ⟨ 𝐺 , 𝐻 ⟩ ∈ RingOps ∧ ( 𝐻 ↾ ( ( ran 𝐺 ∖ { ( GId ‘ 𝐺 ) } ) × ( ran 𝐺 ∖ { ( GId ‘ 𝐺 ) } ) ) ) ∈ GrpOp ) )
18 3 sneqi { 𝑍 } = { ( GId ‘ 𝐺 ) }
19 4 18 difeq12i ( 𝑋 ∖ { 𝑍 } ) = ( ran 𝐺 ∖ { ( GId ‘ 𝐺 ) } )
20 19 19 xpeq12i ( ( 𝑋 ∖ { 𝑍 } ) × ( 𝑋 ∖ { 𝑍 } ) ) = ( ( ran 𝐺 ∖ { ( GId ‘ 𝐺 ) } ) × ( ran 𝐺 ∖ { ( GId ‘ 𝐺 ) } ) )
21 20 reseq2i ( 𝐻 ↾ ( ( 𝑋 ∖ { 𝑍 } ) × ( 𝑋 ∖ { 𝑍 } ) ) ) = ( 𝐻 ↾ ( ( ran 𝐺 ∖ { ( GId ‘ 𝐺 ) } ) × ( ran 𝐺 ∖ { ( GId ‘ 𝐺 ) } ) ) )
22 21 eleq1i ( ( 𝐻 ↾ ( ( 𝑋 ∖ { 𝑍 } ) × ( 𝑋 ∖ { 𝑍 } ) ) ) ∈ GrpOp ↔ ( 𝐻 ↾ ( ( ran 𝐺 ∖ { ( GId ‘ 𝐺 ) } ) × ( ran 𝐺 ∖ { ( GId ‘ 𝐺 ) } ) ) ) ∈ GrpOp )
23 22 anbi2i ( ( ⟨ 𝐺 , 𝐻 ⟩ ∈ RingOps ∧ ( 𝐻 ↾ ( ( 𝑋 ∖ { 𝑍 } ) × ( 𝑋 ∖ { 𝑍 } ) ) ) ∈ GrpOp ) ↔ ( ⟨ 𝐺 , 𝐻 ⟩ ∈ RingOps ∧ ( 𝐻 ↾ ( ( ran 𝐺 ∖ { ( GId ‘ 𝐺 ) } ) × ( ran 𝐺 ∖ { ( GId ‘ 𝐺 ) } ) ) ) ∈ GrpOp ) )
24 17 23 bitr4i ( ⟨ 𝐺 , 𝐻 ⟩ ∈ DivRingOps ↔ ( ⟨ 𝐺 , 𝐻 ⟩ ∈ RingOps ∧ ( 𝐻 ↾ ( ( 𝑋 ∖ { 𝑍 } ) × ( 𝑋 ∖ { 𝑍 } ) ) ) ∈ GrpOp ) )
25 eleq1 ( 𝑅 = ⟨ 𝐺 , 𝐻 ⟩ → ( 𝑅 ∈ DivRingOps ↔ ⟨ 𝐺 , 𝐻 ⟩ ∈ DivRingOps ) )
26 eleq1 ( 𝑅 = ⟨ 𝐺 , 𝐻 ⟩ → ( 𝑅 ∈ RingOps ↔ ⟨ 𝐺 , 𝐻 ⟩ ∈ RingOps ) )
27 26 anbi1d ( 𝑅 = ⟨ 𝐺 , 𝐻 ⟩ → ( ( 𝑅 ∈ RingOps ∧ ( 𝐻 ↾ ( ( 𝑋 ∖ { 𝑍 } ) × ( 𝑋 ∖ { 𝑍 } ) ) ) ∈ GrpOp ) ↔ ( ⟨ 𝐺 , 𝐻 ⟩ ∈ RingOps ∧ ( 𝐻 ↾ ( ( 𝑋 ∖ { 𝑍 } ) × ( 𝑋 ∖ { 𝑍 } ) ) ) ∈ GrpOp ) ) )
28 25 27 bibi12d ( 𝑅 = ⟨ 𝐺 , 𝐻 ⟩ → ( ( 𝑅 ∈ DivRingOps ↔ ( 𝑅 ∈ RingOps ∧ ( 𝐻 ↾ ( ( 𝑋 ∖ { 𝑍 } ) × ( 𝑋 ∖ { 𝑍 } ) ) ) ∈ GrpOp ) ) ↔ ( ⟨ 𝐺 , 𝐻 ⟩ ∈ DivRingOps ↔ ( ⟨ 𝐺 , 𝐻 ⟩ ∈ RingOps ∧ ( 𝐻 ↾ ( ( 𝑋 ∖ { 𝑍 } ) × ( 𝑋 ∖ { 𝑍 } ) ) ) ∈ GrpOp ) ) ) )
29 24 28 mpbiri ( 𝑅 = ⟨ 𝐺 , 𝐻 ⟩ → ( 𝑅 ∈ DivRingOps ↔ ( 𝑅 ∈ RingOps ∧ ( 𝐻 ↾ ( ( 𝑋 ∖ { 𝑍 } ) × ( 𝑋 ∖ { 𝑍 } ) ) ) ∈ GrpOp ) ) )
30 14 29 sylbir ( 𝑅 = ⟨ ( 1st𝑅 ) , ( 2nd𝑅 ) ⟩ → ( 𝑅 ∈ DivRingOps ↔ ( 𝑅 ∈ RingOps ∧ ( 𝐻 ↾ ( ( 𝑋 ∖ { 𝑍 } ) × ( 𝑋 ∖ { 𝑍 } ) ) ) ∈ GrpOp ) ) )
31 8 12 30 pm5.21nii ( 𝑅 ∈ DivRingOps ↔ ( 𝑅 ∈ RingOps ∧ ( 𝐻 ↾ ( ( 𝑋 ∖ { 𝑍 } ) × ( 𝑋 ∖ { 𝑍 } ) ) ) ∈ GrpOp ) )