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

Metamath Proof Explorer

Theorem isdivrngo

Description: The predicate "is a division ring". (Contributed by FL, 6-Sep-2009) (New usage is discouraged.)

Ref Expression
Assertion isdivrngo ( 𝐻 ∈ 𝐴 → ( ⟨ 𝐺 , 𝐻 ⟩ ∈ DivRingOps ↔ ( ⟨ 𝐺 , 𝐻 ⟩ ∈ RingOps ∧ ( 𝐻 ↾ ( ( ran 𝐺 ∖ { ( GId ‘ 𝐺 ) } ) × ( ran 𝐺 ∖ { ( GId ‘ 𝐺 ) } ) ) ) ∈ GrpOp ) ) )

Proof

Step Hyp Ref Expression
1 df-br ⊢ ( 𝐺 DivRingOps 𝐻 ↔ ⟨ 𝐺 , 𝐻 ⟩ ∈ DivRingOps )
2 df-drngo ⊢ DivRingOps = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ RingOps ∧ ( 𝑦 ↾ ( ( ran 𝑥 ∖ { ( GId ‘ 𝑥 ) } ) × ( ran 𝑥 ∖ { ( GId ‘ 𝑥 ) } ) ) ) ∈ GrpOp ) }
3 2 relopabiv ⊢ Rel DivRingOps
4 3 brrelex1i ⊢ ( 𝐺 DivRingOps 𝐻 → 𝐺 ∈ V )
5 1 4 sylbir ⊢ ( ⟨ 𝐺 , 𝐻 ⟩ ∈ DivRingOps → 𝐺 ∈ V )
6 5 anim1i ⊢ ( ( ⟨ 𝐺 , 𝐻 ⟩ ∈ DivRingOps ∧ 𝐻 ∈ 𝐴 ) → ( 𝐺 ∈ V ∧ 𝐻 ∈ 𝐴 ) )
7 6 ancoms ⊢ ( ( 𝐻 ∈ 𝐴 ∧ ⟨ 𝐺 , 𝐻 ⟩ ∈ DivRingOps ) → ( 𝐺 ∈ V ∧ 𝐻 ∈ 𝐴 ) )
8 rngoablo2 ⊢ ( ⟨ 𝐺 , 𝐻 ⟩ ∈ RingOps → 𝐺 ∈ AbelOp )
9 elex ⊢ ( 𝐺 ∈ AbelOp → 𝐺 ∈ V )
10 8 9 syl ⊢ ( ⟨ 𝐺 , 𝐻 ⟩ ∈ RingOps → 𝐺 ∈ V )
11 10 ad2antrl ⊢ ( ( 𝐻 ∈ 𝐴 ∧ ( ⟨ 𝐺 , 𝐻 ⟩ ∈ RingOps ∧ ( 𝐻 ↾ ( ( ran 𝐺 ∖ { ( GId ‘ 𝐺 ) } ) × ( ran 𝐺 ∖ { ( GId ‘ 𝐺 ) } ) ) ) ∈ GrpOp ) ) → 𝐺 ∈ V )
12 simpl ⊢ ( ( 𝐻 ∈ 𝐴 ∧ ( ⟨ 𝐺 , 𝐻 ⟩ ∈ RingOps ∧ ( 𝐻 ↾ ( ( ran 𝐺 ∖ { ( GId ‘ 𝐺 ) } ) × ( ran 𝐺 ∖ { ( GId ‘ 𝐺 ) } ) ) ) ∈ GrpOp ) ) → 𝐻 ∈ 𝐴 )
13 11 12 jca ⊢ ( ( 𝐻 ∈ 𝐴 ∧ ( ⟨ 𝐺 , 𝐻 ⟩ ∈ RingOps ∧ ( 𝐻 ↾ ( ( ran 𝐺 ∖ { ( GId ‘ 𝐺 ) } ) × ( ran 𝐺 ∖ { ( GId ‘ 𝐺 ) } ) ) ) ∈ GrpOp ) ) → ( 𝐺 ∈ V ∧ 𝐻 ∈ 𝐴 ) )
14 df-drngo ⊢ DivRingOps = { ⟨ 𝑔 , ℎ ⟩ ∣ ( ⟨ 𝑔 , ℎ ⟩ ∈ RingOps ∧ ( ℎ ↾ ( ( ran 𝑔 ∖ { ( GId ‘ 𝑔 ) } ) × ( ran 𝑔 ∖ { ( GId ‘ 𝑔 ) } ) ) ) ∈ GrpOp ) }
15 14 eleq2i ⊢ ( ⟨ 𝐺 , 𝐻 ⟩ ∈ DivRingOps ↔ ⟨ 𝐺 , 𝐻 ⟩ ∈ { ⟨ 𝑔 , ℎ ⟩ ∣ ( ⟨ 𝑔 , ℎ ⟩ ∈ RingOps ∧ ( ℎ ↾ ( ( ran 𝑔 ∖ { ( GId ‘ 𝑔 ) } ) × ( ran 𝑔 ∖ { ( GId ‘ 𝑔 ) } ) ) ) ∈ GrpOp ) } )
16 opeq1 ⊢ ( 𝑔 = 𝐺 → ⟨ 𝑔 , ℎ ⟩ = ⟨ 𝐺 , ℎ ⟩ )
17 16 eleq1d ⊢ ( 𝑔 = 𝐺 → ( ⟨ 𝑔 , ℎ ⟩ ∈ RingOps ↔ ⟨ 𝐺 , ℎ ⟩ ∈ RingOps ) )
18 rneq ⊢ ( 𝑔 = 𝐺 → ran 𝑔 = ran 𝐺 )
19 fveq2 ⊢ ( 𝑔 = 𝐺 → ( GId ‘ 𝑔 ) = ( GId ‘ 𝐺 ) )
20 19 sneqd ⊢ ( 𝑔 = 𝐺 → { ( GId ‘ 𝑔 ) } = { ( GId ‘ 𝐺 ) } )
21 18 20 difeq12d ⊢ ( 𝑔 = 𝐺 → ( ran 𝑔 ∖ { ( GId ‘ 𝑔 ) } ) = ( ran 𝐺 ∖ { ( GId ‘ 𝐺 ) } ) )
22 21 sqxpeqd ⊢ ( 𝑔 = 𝐺 → ( ( ran 𝑔 ∖ { ( GId ‘ 𝑔 ) } ) × ( ran 𝑔 ∖ { ( GId ‘ 𝑔 ) } ) ) = ( ( ran 𝐺 ∖ { ( GId ‘ 𝐺 ) } ) × ( ran 𝐺 ∖ { ( GId ‘ 𝐺 ) } ) ) )
23 22 reseq2d ⊢ ( 𝑔 = 𝐺 → ( ℎ ↾ ( ( ran 𝑔 ∖ { ( GId ‘ 𝑔 ) } ) × ( ran 𝑔 ∖ { ( GId ‘ 𝑔 ) } ) ) ) = ( ℎ ↾ ( ( ran 𝐺 ∖ { ( GId ‘ 𝐺 ) } ) × ( ran 𝐺 ∖ { ( GId ‘ 𝐺 ) } ) ) ) )
24 23 eleq1d ⊢ ( 𝑔 = 𝐺 → ( ( ℎ ↾ ( ( ran 𝑔 ∖ { ( GId ‘ 𝑔 ) } ) × ( ran 𝑔 ∖ { ( GId ‘ 𝑔 ) } ) ) ) ∈ GrpOp ↔ ( ℎ ↾ ( ( ran 𝐺 ∖ { ( GId ‘ 𝐺 ) } ) × ( ran 𝐺 ∖ { ( GId ‘ 𝐺 ) } ) ) ) ∈ GrpOp ) )
25 17 24 anbi12d ⊢ ( 𝑔 = 𝐺 → ( ( ⟨ 𝑔 , ℎ ⟩ ∈ RingOps ∧ ( ℎ ↾ ( ( ran 𝑔 ∖ { ( GId ‘ 𝑔 ) } ) × ( ran 𝑔 ∖ { ( GId ‘ 𝑔 ) } ) ) ) ∈ GrpOp ) ↔ ( ⟨ 𝐺 , ℎ ⟩ ∈ RingOps ∧ ( ℎ ↾ ( ( ran 𝐺 ∖ { ( GId ‘ 𝐺 ) } ) × ( ran 𝐺 ∖ { ( GId ‘ 𝐺 ) } ) ) ) ∈ GrpOp ) ) )
26 opeq2 ⊢ ( ℎ = 𝐻 → ⟨ 𝐺 , ℎ ⟩ = ⟨ 𝐺 , 𝐻 ⟩ )
27 26 eleq1d ⊢ ( ℎ = 𝐻 → ( ⟨ 𝐺 , ℎ ⟩ ∈ RingOps ↔ ⟨ 𝐺 , 𝐻 ⟩ ∈ RingOps ) )
28 reseq1 ⊢ ( ℎ = 𝐻 → ( ℎ ↾ ( ( ran 𝐺 ∖ { ( GId ‘ 𝐺 ) } ) × ( ran 𝐺 ∖ { ( GId ‘ 𝐺 ) } ) ) ) = ( 𝐻 ↾ ( ( ran 𝐺 ∖ { ( GId ‘ 𝐺 ) } ) × ( ran 𝐺 ∖ { ( GId ‘ 𝐺 ) } ) ) ) )
29 28 eleq1d ⊢ ( ℎ = 𝐻 → ( ( ℎ ↾ ( ( ran 𝐺 ∖ { ( GId ‘ 𝐺 ) } ) × ( ran 𝐺 ∖ { ( GId ‘ 𝐺 ) } ) ) ) ∈ GrpOp ↔ ( 𝐻 ↾ ( ( ran 𝐺 ∖ { ( GId ‘ 𝐺 ) } ) × ( ran 𝐺 ∖ { ( GId ‘ 𝐺 ) } ) ) ) ∈ GrpOp ) )
30 27 29 anbi12d ⊢ ( ℎ = 𝐻 → ( ( ⟨ 𝐺 , ℎ ⟩ ∈ RingOps ∧ ( ℎ ↾ ( ( ran 𝐺 ∖ { ( GId ‘ 𝐺 ) } ) × ( ran 𝐺 ∖ { ( GId ‘ 𝐺 ) } ) ) ) ∈ GrpOp ) ↔ ( ⟨ 𝐺 , 𝐻 ⟩ ∈ RingOps ∧ ( 𝐻 ↾ ( ( ran 𝐺 ∖ { ( GId ‘ 𝐺 ) } ) × ( ran 𝐺 ∖ { ( GId ‘ 𝐺 ) } ) ) ) ∈ GrpOp ) ) )
31 25 30 opelopabg ⊢ ( ( 𝐺 ∈ V ∧ 𝐻 ∈ 𝐴 ) → ( ⟨ 𝐺 , 𝐻 ⟩ ∈ { ⟨ 𝑔 , ℎ ⟩ ∣ ( ⟨ 𝑔 , ℎ ⟩ ∈ RingOps ∧ ( ℎ ↾ ( ( ran 𝑔 ∖ { ( GId ‘ 𝑔 ) } ) × ( ran 𝑔 ∖ { ( GId ‘ 𝑔 ) } ) ) ) ∈ GrpOp ) } ↔ ( ⟨ 𝐺 , 𝐻 ⟩ ∈ RingOps ∧ ( 𝐻 ↾ ( ( ran 𝐺 ∖ { ( GId ‘ 𝐺 ) } ) × ( ran 𝐺 ∖ { ( GId ‘ 𝐺 ) } ) ) ) ∈ GrpOp ) ) )
32 15 31 bitrid ⊢ ( ( 𝐺 ∈ V ∧ 𝐻 ∈ 𝐴 ) → ( ⟨ 𝐺 , 𝐻 ⟩ ∈ DivRingOps ↔ ( ⟨ 𝐺 , 𝐻 ⟩ ∈ RingOps ∧ ( 𝐻 ↾ ( ( ran 𝐺 ∖ { ( GId ‘ 𝐺 ) } ) × ( ran 𝐺 ∖ { ( GId ‘ 𝐺 ) } ) ) ) ∈ GrpOp ) ) )
33 7 13 32 pm5.21nd ⊢ ( 𝐻 ∈ 𝐴 → ( ⟨ 𝐺 , 𝐻 ⟩ ∈ DivRingOps ↔ ( ⟨ 𝐺 , 𝐻 ⟩ ∈ RingOps ∧ ( 𝐻 ↾ ( ( ran 𝐺 ∖ { ( GId ‘ 𝐺 ) } ) × ( ran 𝐺 ∖ { ( GId ‘ 𝐺 ) } ) ) ) ∈ GrpOp ) ) )