This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) )