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	syl5bb	⊢ ( ( 𝐺 ∈ V ∧ 𝐻 ∈ 𝐴 ) → ( ⟨ 𝐺 , 𝐻 ⟩ ∈ DivRingOps ↔ ( ⟨ 𝐺 , 𝐻 ⟩ ∈ RingOps ∧ ( 𝐻 ↾ ( ( ran 𝐺 ∖ { ( GId ‘ 𝐺 ) } ) × ( ran 𝐺 ∖ { ( GId ‘ 𝐺 ) } ) ) ) ∈ GrpOp ) ) )
33	7 13 32	pm5.21nd	⊢ ( 𝐻 ∈ 𝐴 → ( ⟨ 𝐺 , 𝐻 ⟩ ∈ DivRingOps ↔ ( ⟨ 𝐺 , 𝐻 ⟩ ∈ RingOps ∧ ( 𝐻 ↾ ( ( ran 𝐺 ∖ { ( GId ‘ 𝐺 ) } ) × ( ran 𝐺 ∖ { ( GId ‘ 𝐺 ) } ) ) ) ∈ GrpOp ) ) )