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 ⊢ H ∈ A → G H ∈ DivRingOps ↔ G H ∈ RingOps ∧ H ↾ ran ⁡ G ∖ GId ⁡ G × ran ⁡ G ∖ GId ⁡ G ∈ GrpOp

Proof

Step Hyp Ref Expression
1 df-br ⊢ G DivRingOps H ↔ G H ∈ DivRingOps
2 df-drngo ⊢ DivRingOps = x y | x y ∈ RingOps ∧ y ↾ ran ⁡ x ∖ GId ⁡ x × ran ⁡ x ∖ GId ⁡ x ∈ GrpOp
3 2 relopabiv ⊢ Rel ⁡ DivRingOps
4 3 brrelex1i ⊢ G DivRingOps H → G ∈ V
5 1 4 sylbir ⊢ G H ∈ DivRingOps → G ∈ V
6 5 anim1i ⊢ G H ∈ DivRingOps ∧ H ∈ A → G ∈ V ∧ H ∈ A
7 6 ancoms ⊢ H ∈ A ∧ G H ∈ DivRingOps → G ∈ V ∧ H ∈ A
8 rngoablo2 ⊢ G H ∈ RingOps → G ∈ AbelOp
9 elex ⊢ G ∈ AbelOp → G ∈ V
10 8 9 syl ⊢ G H ∈ RingOps → G ∈ V
11 10 ad2antrl ⊢ H ∈ A ∧ G H ∈ RingOps ∧ H ↾ ran ⁡ G ∖ GId ⁡ G × ran ⁡ G ∖ GId ⁡ G ∈ GrpOp → G ∈ V
12 simpl ⊢ H ∈ A ∧ G H ∈ RingOps ∧ H ↾ ran ⁡ G ∖ GId ⁡ G × ran ⁡ G ∖ GId ⁡ G ∈ GrpOp → H ∈ A
13 11 12 jca ⊢ H ∈ A ∧ G H ∈ RingOps ∧ H ↾ ran ⁡ G ∖ GId ⁡ G × ran ⁡ G ∖ GId ⁡ G ∈ GrpOp → G ∈ V ∧ H ∈ A
14 df-drngo ⊢ DivRingOps = g h | g h ∈ RingOps ∧ h ↾ ran ⁡ g ∖ GId ⁡ g × ran ⁡ g ∖ GId ⁡ g ∈ GrpOp
15 14 eleq2i ⊢ G H ∈ DivRingOps ↔ G H ∈ g h | g h ∈ RingOps ∧ h ↾ ran ⁡ g ∖ GId ⁡ g × ran ⁡ g ∖ GId ⁡ g ∈ GrpOp
16 opeq1 ⊢ g = G → g h = G h
17 16 eleq1d ⊢ g = G → g h ∈ RingOps ↔ G h ∈ RingOps
18 rneq ⊢ g = G → ran ⁡ g = ran ⁡ G
19 fveq2 ⊢ g = G → GId ⁡ g = GId ⁡ G
20 19 sneqd ⊢ g = G → GId ⁡ g = GId ⁡ G
21 18 20 difeq12d ⊢ g = G → ran ⁡ g ∖ GId ⁡ g = ran ⁡ G ∖ GId ⁡ G
22 21 sqxpeqd ⊢ g = G → ran ⁡ g ∖ GId ⁡ g × ran ⁡ g ∖ GId ⁡ g = ran ⁡ G ∖ GId ⁡ G × ran ⁡ G ∖ GId ⁡ G
23 22 reseq2d ⊢ g = G → h ↾ ran ⁡ g ∖ GId ⁡ g × ran ⁡ g ∖ GId ⁡ g = h ↾ ran ⁡ G ∖ GId ⁡ G × ran ⁡ G ∖ GId ⁡ G
24 23 eleq1d ⊢ g = G → h ↾ ran ⁡ g ∖ GId ⁡ g × ran ⁡ g ∖ GId ⁡ g ∈ GrpOp ↔ h ↾ ran ⁡ G ∖ GId ⁡ G × ran ⁡ G ∖ GId ⁡ G ∈ GrpOp
25 17 24 anbi12d ⊢ g = G → g h ∈ RingOps ∧ h ↾ ran ⁡ g ∖ GId ⁡ g × ran ⁡ g ∖ GId ⁡ g ∈ GrpOp ↔ G h ∈ RingOps ∧ h ↾ ran ⁡ G ∖ GId ⁡ G × ran ⁡ G ∖ GId ⁡ G ∈ GrpOp
26 opeq2 ⊢ h = H → G h = G H
27 26 eleq1d ⊢ h = H → G h ∈ RingOps ↔ G H ∈ RingOps
28 reseq1 ⊢ h = H → h ↾ ran ⁡ G ∖ GId ⁡ G × ran ⁡ G ∖ GId ⁡ G = H ↾ ran ⁡ G ∖ GId ⁡ G × ran ⁡ G ∖ GId ⁡ G
29 28 eleq1d ⊢ h = H → h ↾ ran ⁡ G ∖ GId ⁡ G × ran ⁡ G ∖ GId ⁡ G ∈ GrpOp ↔ H ↾ ran ⁡ G ∖ GId ⁡ G × ran ⁡ G ∖ GId ⁡ G ∈ GrpOp
30 27 29 anbi12d ⊢ h = H → G h ∈ RingOps ∧ h ↾ ran ⁡ G ∖ GId ⁡ G × ran ⁡ G ∖ GId ⁡ G ∈ GrpOp ↔ G H ∈ RingOps ∧ H ↾ ran ⁡ G ∖ GId ⁡ G × ran ⁡ G ∖ GId ⁡ G ∈ GrpOp
31 25 30 opelopabg ⊢ G ∈ V ∧ H ∈ A → G H ∈ g h | g h ∈ RingOps ∧ h ↾ ran ⁡ g ∖ GId ⁡ g × ran ⁡ g ∖ GId ⁡ g ∈ GrpOp ↔ G H ∈ RingOps ∧ H ↾ ran ⁡ G ∖ GId ⁡ G × ran ⁡ G ∖ GId ⁡ G ∈ GrpOp
32 15 31 syl5bb ⊢ G ∈ V ∧ H ∈ A → G H ∈ DivRingOps ↔ G H ∈ RingOps ∧ H ↾ ran ⁡ G ∖ GId ⁡ G × ran ⁡ G ∖ GId ⁡ G ∈ GrpOp
33 7 13 32 pm5.21nd ⊢ H ∈ A → G H ∈ DivRingOps ↔ G H ∈ RingOps ∧ H ↾ ran ⁡ G ∖ GId ⁡ G × ran ⁡ G ∖ GId ⁡ G ∈ GrpOp