Theorem drngoi

Description: The properties of a division ring. (Contributed by NM, 4-Apr-2009) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		drngi.1	⊢ 𝐺 = ( 1st ‘ 𝑅 )
2		drngi.2	⊢ 𝐻 = ( 2nd ‘ 𝑅 )
3		drngi.3	⊢ 𝑋 = ran 𝐺
4		drngi.4	⊢ 𝑍 = ( GId ‘ 𝐺 )
5		opeq1	⊢ ( 𝑔 = ( 1st ‘ 𝑅 ) → ⟨ 𝑔 , ℎ ⟩ = ⟨ ( 1st ‘ 𝑅 ) , ℎ ⟩ )
6	5	eleq1d	⊢ ( 𝑔 = ( 1st ‘ 𝑅 ) → ( ⟨ 𝑔 , ℎ ⟩ ∈ RingOps ↔ ⟨ ( 1st ‘ 𝑅 ) , ℎ ⟩ ∈ RingOps ) )
7		id	⊢ ( 𝑔 = ( 1st ‘ 𝑅 ) → 𝑔 = ( 1st ‘ 𝑅 ) )
8	7 1	eqtr4di	⊢ ( 𝑔 = ( 1st ‘ 𝑅 ) → 𝑔 = 𝐺 )
9	8	rneqd	⊢ ( 𝑔 = ( 1st ‘ 𝑅 ) → ran 𝑔 = ran 𝐺 )
10	9 3	eqtr4di	⊢ ( 𝑔 = ( 1st ‘ 𝑅 ) → ran 𝑔 = 𝑋 )
11	8	fveq2d	⊢ ( 𝑔 = ( 1st ‘ 𝑅 ) → ( GId ‘ 𝑔 ) = ( GId ‘ 𝐺 ) )
12	11 4	eqtr4di	⊢ ( 𝑔 = ( 1st ‘ 𝑅 ) → ( GId ‘ 𝑔 ) = 𝑍 )
13	12	sneqd	⊢ ( 𝑔 = ( 1st ‘ 𝑅 ) → { ( GId ‘ 𝑔 ) } = { 𝑍 } )
14	10 13	difeq12d	⊢ ( 𝑔 = ( 1st ‘ 𝑅 ) → ( ran 𝑔 ∖ { ( GId ‘ 𝑔 ) } ) = ( 𝑋 ∖ { 𝑍 } ) )
15	14	sqxpeqd	⊢ ( 𝑔 = ( 1st ‘ 𝑅 ) → ( ( ran 𝑔 ∖ { ( GId ‘ 𝑔 ) } ) × ( ran 𝑔 ∖ { ( GId ‘ 𝑔 ) } ) ) = ( ( 𝑋 ∖ { 𝑍 } ) × ( 𝑋 ∖ { 𝑍 } ) ) )
16	15	reseq2d	⊢ ( 𝑔 = ( 1st ‘ 𝑅 ) → ( ℎ ↾ ( ( ran 𝑔 ∖ { ( GId ‘ 𝑔 ) } ) × ( ran 𝑔 ∖ { ( GId ‘ 𝑔 ) } ) ) ) = ( ℎ ↾ ( ( 𝑋 ∖ { 𝑍 } ) × ( 𝑋 ∖ { 𝑍 } ) ) ) )
17	16	eleq1d	⊢ ( 𝑔 = ( 1st ‘ 𝑅 ) → ( ( ℎ ↾ ( ( ran 𝑔 ∖ { ( GId ‘ 𝑔 ) } ) × ( ran 𝑔 ∖ { ( GId ‘ 𝑔 ) } ) ) ) ∈ GrpOp ↔ ( ℎ ↾ ( ( 𝑋 ∖ { 𝑍 } ) × ( 𝑋 ∖ { 𝑍 } ) ) ) ∈ GrpOp ) )
18	6 17	anbi12d	⊢ ( 𝑔 = ( 1st ‘ 𝑅 ) → ( ( ⟨ 𝑔 , ℎ ⟩ ∈ RingOps ∧ ( ℎ ↾ ( ( ran 𝑔 ∖ { ( GId ‘ 𝑔 ) } ) × ( ran 𝑔 ∖ { ( GId ‘ 𝑔 ) } ) ) ) ∈ GrpOp ) ↔ ( ⟨ ( 1st ‘ 𝑅 ) , ℎ ⟩ ∈ RingOps ∧ ( ℎ ↾ ( ( 𝑋 ∖ { 𝑍 } ) × ( 𝑋 ∖ { 𝑍 } ) ) ) ∈ GrpOp ) ) )
19		opeq2	⊢ ( ℎ = ( 2nd ‘ 𝑅 ) → ⟨ ( 1st ‘ 𝑅 ) , ℎ ⟩ = ⟨ ( 1st ‘ 𝑅 ) , ( 2nd ‘ 𝑅 ) ⟩ )
20	19	eleq1d	⊢ ( ℎ = ( 2nd ‘ 𝑅 ) → ( ⟨ ( 1st ‘ 𝑅 ) , ℎ ⟩ ∈ RingOps ↔ ⟨ ( 1st ‘ 𝑅 ) , ( 2nd ‘ 𝑅 ) ⟩ ∈ RingOps ) )
21	20	anbi1d	⊢ ( ℎ = ( 2nd ‘ 𝑅 ) → ( ( ⟨ ( 1st ‘ 𝑅 ) , ℎ ⟩ ∈ RingOps ∧ ( ℎ ↾ ( ( 𝑋 ∖ { 𝑍 } ) × ( 𝑋 ∖ { 𝑍 } ) ) ) ∈ GrpOp ) ↔ ( ⟨ ( 1st ‘ 𝑅 ) , ( 2nd ‘ 𝑅 ) ⟩ ∈ RingOps ∧ ( ℎ ↾ ( ( 𝑋 ∖ { 𝑍 } ) × ( 𝑋 ∖ { 𝑍 } ) ) ) ∈ GrpOp ) ) )
22		id	⊢ ( ℎ = ( 2nd ‘ 𝑅 ) → ℎ = ( 2nd ‘ 𝑅 ) )
23	2 22	eqtr4id	⊢ ( ℎ = ( 2nd ‘ 𝑅 ) → 𝐻 = ℎ )
24	23	reseq1d	⊢ ( ℎ = ( 2nd ‘ 𝑅 ) → ( 𝐻 ↾ ( ( 𝑋 ∖ { 𝑍 } ) × ( 𝑋 ∖ { 𝑍 } ) ) ) = ( ℎ ↾ ( ( 𝑋 ∖ { 𝑍 } ) × ( 𝑋 ∖ { 𝑍 } ) ) ) )
25	24	eleq1d	⊢ ( ℎ = ( 2nd ‘ 𝑅 ) → ( ( 𝐻 ↾ ( ( 𝑋 ∖ { 𝑍 } ) × ( 𝑋 ∖ { 𝑍 } ) ) ) ∈ GrpOp ↔ ( ℎ ↾ ( ( 𝑋 ∖ { 𝑍 } ) × ( 𝑋 ∖ { 𝑍 } ) ) ) ∈ GrpOp ) )
26	25	anbi2d	⊢ ( ℎ = ( 2nd ‘ 𝑅 ) → ( ( ⟨ ( 1st ‘ 𝑅 ) , ( 2nd ‘ 𝑅 ) ⟩ ∈ RingOps ∧ ( 𝐻 ↾ ( ( 𝑋 ∖ { 𝑍 } ) × ( 𝑋 ∖ { 𝑍 } ) ) ) ∈ GrpOp ) ↔ ( ⟨ ( 1st ‘ 𝑅 ) , ( 2nd ‘ 𝑅 ) ⟩ ∈ RingOps ∧ ( ℎ ↾ ( ( 𝑋 ∖ { 𝑍 } ) × ( 𝑋 ∖ { 𝑍 } ) ) ) ∈ GrpOp ) ) )
27	21 26	bitr4d	⊢ ( ℎ = ( 2nd ‘ 𝑅 ) → ( ( ⟨ ( 1st ‘ 𝑅 ) , ℎ ⟩ ∈ RingOps ∧ ( ℎ ↾ ( ( 𝑋 ∖ { 𝑍 } ) × ( 𝑋 ∖ { 𝑍 } ) ) ) ∈ GrpOp ) ↔ ( ⟨ ( 1st ‘ 𝑅 ) , ( 2nd ‘ 𝑅 ) ⟩ ∈ RingOps ∧ ( 𝐻 ↾ ( ( 𝑋 ∖ { 𝑍 } ) × ( 𝑋 ∖ { 𝑍 } ) ) ) ∈ GrpOp ) ) )
28	18 27	elopabi	⊢ ( 𝑅 ∈ { ⟨ 𝑔 , ℎ ⟩ ∣ ( ⟨ 𝑔 , ℎ ⟩ ∈ RingOps ∧ ( ℎ ↾ ( ( ran 𝑔 ∖ { ( GId ‘ 𝑔 ) } ) × ( ran 𝑔 ∖ { ( GId ‘ 𝑔 ) } ) ) ) ∈ GrpOp ) } → ( ⟨ ( 1st ‘ 𝑅 ) , ( 2nd ‘ 𝑅 ) ⟩ ∈ RingOps ∧ ( 𝐻 ↾ ( ( 𝑋 ∖ { 𝑍 } ) × ( 𝑋 ∖ { 𝑍 } ) ) ) ∈ GrpOp ) )
29		df-drngo	⊢ DivRingOps = { ⟨ 𝑔 , ℎ ⟩ ∣ ( ⟨ 𝑔 , ℎ ⟩ ∈ RingOps ∧ ( ℎ ↾ ( ( ran 𝑔 ∖ { ( GId ‘ 𝑔 ) } ) × ( ran 𝑔 ∖ { ( GId ‘ 𝑔 ) } ) ) ) ∈ GrpOp ) }
30	28 29	eleq2s	⊢ ( 𝑅 ∈ DivRingOps → ( ⟨ ( 1st ‘ 𝑅 ) , ( 2nd ‘ 𝑅 ) ⟩ ∈ RingOps ∧ ( 𝐻 ↾ ( ( 𝑋 ∖ { 𝑍 } ) × ( 𝑋 ∖ { 𝑍 } ) ) ) ∈ GrpOp ) )
31	29	relopabiv	⊢ Rel DivRingOps
32		1st2nd	⊢ ( ( Rel DivRingOps ∧ 𝑅 ∈ DivRingOps ) → 𝑅 = ⟨ ( 1st ‘ 𝑅 ) , ( 2nd ‘ 𝑅 ) ⟩ )
33	31 32	mpan	⊢ ( 𝑅 ∈ DivRingOps → 𝑅 = ⟨ ( 1st ‘ 𝑅 ) , ( 2nd ‘ 𝑅 ) ⟩ )
34	33	eleq1d	⊢ ( 𝑅 ∈ DivRingOps → ( 𝑅 ∈ RingOps ↔ ⟨ ( 1st ‘ 𝑅 ) , ( 2nd ‘ 𝑅 ) ⟩ ∈ RingOps ) )
35	34	anbi1d	⊢ ( 𝑅 ∈ DivRingOps → ( ( 𝑅 ∈ RingOps ∧ ( 𝐻 ↾ ( ( 𝑋 ∖ { 𝑍 } ) × ( 𝑋 ∖ { 𝑍 } ) ) ) ∈ GrpOp ) ↔ ( ⟨ ( 1st ‘ 𝑅 ) , ( 2nd ‘ 𝑅 ) ⟩ ∈ RingOps ∧ ( 𝐻 ↾ ( ( 𝑋 ∖ { 𝑍 } ) × ( 𝑋 ∖ { 𝑍 } ) ) ) ∈ GrpOp ) ) )
36	30 35	mpbird	⊢ ( 𝑅 ∈ DivRingOps → ( 𝑅 ∈ RingOps ∧ ( 𝐻 ↾ ( ( 𝑋 ∖ { 𝑍 } ) × ( 𝑋 ∖ { 𝑍 } ) ) ) ∈ GrpOp ) )