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

Metamath Proof Explorer

Theorem istgp

Description: The predicate "is a topological group". Definition 1 of BourbakiTop1 p. III.1. (Contributed by FL, 18-Apr-2010) (Revised by Mario Carneiro, 13-Aug-2015)

Ref Expression
Hypotheses istgp.1 ⊢ 𝐽 = ( TopOpen ‘ 𝐺 )
istgp.2 ⊢ 𝐼 = ( invg ‘ 𝐺 )
Assertion istgp ( 𝐺 ∈ TopGrp ↔ ( 𝐺 ∈ Grp ∧ 𝐺 ∈ TopMnd ∧ 𝐼 ∈ ( 𝐽 Cn 𝐽 ) ) )

Proof

Step Hyp Ref Expression
1 istgp.1 ⊢ 𝐽 = ( TopOpen ‘ 𝐺 )
2 istgp.2 ⊢ 𝐼 = ( invg ‘ 𝐺 )
3 elin ⊢ ( 𝐺 ∈ ( Grp ∩ TopMnd ) ↔ ( 𝐺 ∈ Grp ∧ 𝐺 ∈ TopMnd ) )
4 3 anbi1i ⊢ ( ( 𝐺 ∈ ( Grp ∩ TopMnd ) ∧ 𝐼 ∈ ( 𝐽 Cn 𝐽 ) ) ↔ ( ( 𝐺 ∈ Grp ∧ 𝐺 ∈ TopMnd ) ∧ 𝐼 ∈ ( 𝐽 Cn 𝐽 ) ) )
5 fvexd ⊢ ( 𝑓 = 𝐺 → ( TopOpen ‘ 𝑓 ) ∈ V )
6 simpl ⊢ ( ( 𝑓 = 𝐺 ∧ 𝑗 = ( TopOpen ‘ 𝑓 ) ) → 𝑓 = 𝐺 )
7 6 fveq2d ⊢ ( ( 𝑓 = 𝐺 ∧ 𝑗 = ( TopOpen ‘ 𝑓 ) ) → ( invg ‘ 𝑓 ) = ( invg ‘ 𝐺 ) )
8 7 2 eqtr4di ⊢ ( ( 𝑓 = 𝐺 ∧ 𝑗 = ( TopOpen ‘ 𝑓 ) ) → ( invg ‘ 𝑓 ) = 𝐼 )
9 id ⊢ ( 𝑗 = ( TopOpen ‘ 𝑓 ) → 𝑗 = ( TopOpen ‘ 𝑓 ) )
10 fveq2 ⊢ ( 𝑓 = 𝐺 → ( TopOpen ‘ 𝑓 ) = ( TopOpen ‘ 𝐺 ) )
11 10 1 eqtr4di ⊢ ( 𝑓 = 𝐺 → ( TopOpen ‘ 𝑓 ) = 𝐽 )
12 9 11 sylan9eqr ⊢ ( ( 𝑓 = 𝐺 ∧ 𝑗 = ( TopOpen ‘ 𝑓 ) ) → 𝑗 = 𝐽 )
13 12 12 oveq12d ⊢ ( ( 𝑓 = 𝐺 ∧ 𝑗 = ( TopOpen ‘ 𝑓 ) ) → ( 𝑗 Cn 𝑗 ) = ( 𝐽 Cn 𝐽 ) )
14 8 13 eleq12d ⊢ ( ( 𝑓 = 𝐺 ∧ 𝑗 = ( TopOpen ‘ 𝑓 ) ) → ( ( invg ‘ 𝑓 ) ∈ ( 𝑗 Cn 𝑗 ) ↔ 𝐼 ∈ ( 𝐽 Cn 𝐽 ) ) )
15 5 14 sbcied ⊢ ( 𝑓 = 𝐺 → ( [ ( TopOpen ‘ 𝑓 ) / 𝑗 ] ( invg ‘ 𝑓 ) ∈ ( 𝑗 Cn 𝑗 ) ↔ 𝐼 ∈ ( 𝐽 Cn 𝐽 ) ) )
16 df-tgp ⊢ TopGrp = { 𝑓 ∈ ( Grp ∩ TopMnd ) ∣ [ ( TopOpen ‘ 𝑓 ) / 𝑗 ] ( invg ‘ 𝑓 ) ∈ ( 𝑗 Cn 𝑗 ) }
17 15 16 elrab2 ⊢ ( 𝐺 ∈ TopGrp ↔ ( 𝐺 ∈ ( Grp ∩ TopMnd ) ∧ 𝐼 ∈ ( 𝐽 Cn 𝐽 ) ) )
18 df-3an ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐺 ∈ TopMnd ∧ 𝐼 ∈ ( 𝐽 Cn 𝐽 ) ) ↔ ( ( 𝐺 ∈ Grp ∧ 𝐺 ∈ TopMnd ) ∧ 𝐼 ∈ ( 𝐽 Cn 𝐽 ) ) )
19 4 17 18 3bitr4i ⊢ ( 𝐺 ∈ TopGrp ↔ ( 𝐺 ∈ Grp ∧ 𝐺 ∈ TopMnd ∧ 𝐼 ∈ ( 𝐽 Cn 𝐽 ) ) )