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