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

Metamath Proof Explorer

Theorem isnsg2

Description: Weaken the condition of isnsg to only one side of the implication. (Contributed by Mario Carneiro, 18-Jan-2015)

Ref Expression
Hypotheses isnsg.1 ⊢ 𝑋 = ( Base ‘ 𝐺 )
isnsg.2 ⊢ + = ( +g ‘ 𝐺 )
Assertion isnsg2 ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ↔ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 + 𝑦 ) ∈ 𝑆 → ( 𝑦 + 𝑥 ) ∈ 𝑆 ) ) )

Proof

Step Hyp Ref Expression
1 isnsg.1 ⊢ 𝑋 = ( Base ‘ 𝐺 )
2 isnsg.2 ⊢ + = ( +g ‘ 𝐺 )
3 1 2 isnsg ⊢ ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ↔ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( 𝑥 + 𝑧 ) ∈ 𝑆 ↔ ( 𝑧 + 𝑥 ) ∈ 𝑆 ) ) )
4 dfbi2 ⊢ ( ( ( 𝑥 + 𝑧 ) ∈ 𝑆 ↔ ( 𝑧 + 𝑥 ) ∈ 𝑆 ) ↔ ( ( ( 𝑥 + 𝑧 ) ∈ 𝑆 → ( 𝑧 + 𝑥 ) ∈ 𝑆 ) ∧ ( ( 𝑧 + 𝑥 ) ∈ 𝑆 → ( 𝑥 + 𝑧 ) ∈ 𝑆 ) ) )
5 4 ralbii ⊢ ( ∀ 𝑧 ∈ 𝑋 ( ( 𝑥 + 𝑧 ) ∈ 𝑆 ↔ ( 𝑧 + 𝑥 ) ∈ 𝑆 ) ↔ ∀ 𝑧 ∈ 𝑋 ( ( ( 𝑥 + 𝑧 ) ∈ 𝑆 → ( 𝑧 + 𝑥 ) ∈ 𝑆 ) ∧ ( ( 𝑧 + 𝑥 ) ∈ 𝑆 → ( 𝑥 + 𝑧 ) ∈ 𝑆 ) ) )
6 5 ralbii ⊢ ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( 𝑥 + 𝑧 ) ∈ 𝑆 ↔ ( 𝑧 + 𝑥 ) ∈ 𝑆 ) ↔ ∀ 𝑥 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( ( 𝑥 + 𝑧 ) ∈ 𝑆 → ( 𝑧 + 𝑥 ) ∈ 𝑆 ) ∧ ( ( 𝑧 + 𝑥 ) ∈ 𝑆 → ( 𝑥 + 𝑧 ) ∈ 𝑆 ) ) )
7 r19.26-2 ⊢ ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( ( 𝑥 + 𝑧 ) ∈ 𝑆 → ( 𝑧 + 𝑥 ) ∈ 𝑆 ) ∧ ( ( 𝑧 + 𝑥 ) ∈ 𝑆 → ( 𝑥 + 𝑧 ) ∈ 𝑆 ) ) ↔ ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( 𝑥 + 𝑧 ) ∈ 𝑆 → ( 𝑧 + 𝑥 ) ∈ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( 𝑧 + 𝑥 ) ∈ 𝑆 → ( 𝑥 + 𝑧 ) ∈ 𝑆 ) ) )
8 6 7 bitri ⊢ ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( 𝑥 + 𝑧 ) ∈ 𝑆 ↔ ( 𝑧 + 𝑥 ) ∈ 𝑆 ) ↔ ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( 𝑥 + 𝑧 ) ∈ 𝑆 → ( 𝑧 + 𝑥 ) ∈ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( 𝑧 + 𝑥 ) ∈ 𝑆 → ( 𝑥 + 𝑧 ) ∈ 𝑆 ) ) )
9 oveq2 ⊢ ( 𝑧 = 𝑦 → ( 𝑥 + 𝑧 ) = ( 𝑥 + 𝑦 ) )
10 9 eleq1d ⊢ ( 𝑧 = 𝑦 → ( ( 𝑥 + 𝑧 ) ∈ 𝑆 ↔ ( 𝑥 + 𝑦 ) ∈ 𝑆 ) )
11 oveq1 ⊢ ( 𝑧 = 𝑦 → ( 𝑧 + 𝑥 ) = ( 𝑦 + 𝑥 ) )
12 11 eleq1d ⊢ ( 𝑧 = 𝑦 → ( ( 𝑧 + 𝑥 ) ∈ 𝑆 ↔ ( 𝑦 + 𝑥 ) ∈ 𝑆 ) )
13 10 12 imbi12d ⊢ ( 𝑧 = 𝑦 → ( ( ( 𝑥 + 𝑧 ) ∈ 𝑆 → ( 𝑧 + 𝑥 ) ∈ 𝑆 ) ↔ ( ( 𝑥 + 𝑦 ) ∈ 𝑆 → ( 𝑦 + 𝑥 ) ∈ 𝑆 ) ) )
14 13 cbvralvw ⊢ ( ∀ 𝑧 ∈ 𝑋 ( ( 𝑥 + 𝑧 ) ∈ 𝑆 → ( 𝑧 + 𝑥 ) ∈ 𝑆 ) ↔ ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 + 𝑦 ) ∈ 𝑆 → ( 𝑦 + 𝑥 ) ∈ 𝑆 ) )
15 14 ralbii ⊢ ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( 𝑥 + 𝑧 ) ∈ 𝑆 → ( 𝑧 + 𝑥 ) ∈ 𝑆 ) ↔ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 + 𝑦 ) ∈ 𝑆 → ( 𝑦 + 𝑥 ) ∈ 𝑆 ) )
16 ralcom ⊢ ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( 𝑧 + 𝑥 ) ∈ 𝑆 → ( 𝑥 + 𝑧 ) ∈ 𝑆 ) ↔ ∀ 𝑧 ∈ 𝑋 ∀ 𝑥 ∈ 𝑋 ( ( 𝑧 + 𝑥 ) ∈ 𝑆 → ( 𝑥 + 𝑧 ) ∈ 𝑆 ) )
17 oveq2 ⊢ ( 𝑥 = 𝑦 → ( 𝑧 + 𝑥 ) = ( 𝑧 + 𝑦 ) )
18 17 eleq1d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑧 + 𝑥 ) ∈ 𝑆 ↔ ( 𝑧 + 𝑦 ) ∈ 𝑆 ) )
19 oveq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 + 𝑧 ) = ( 𝑦 + 𝑧 ) )
20 19 eleq1d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 + 𝑧 ) ∈ 𝑆 ↔ ( 𝑦 + 𝑧 ) ∈ 𝑆 ) )
21 18 20 imbi12d ⊢ ( 𝑥 = 𝑦 → ( ( ( 𝑧 + 𝑥 ) ∈ 𝑆 → ( 𝑥 + 𝑧 ) ∈ 𝑆 ) ↔ ( ( 𝑧 + 𝑦 ) ∈ 𝑆 → ( 𝑦 + 𝑧 ) ∈ 𝑆 ) ) )
22 21 cbvralvw ⊢ ( ∀ 𝑥 ∈ 𝑋 ( ( 𝑧 + 𝑥 ) ∈ 𝑆 → ( 𝑥 + 𝑧 ) ∈ 𝑆 ) ↔ ∀ 𝑦 ∈ 𝑋 ( ( 𝑧 + 𝑦 ) ∈ 𝑆 → ( 𝑦 + 𝑧 ) ∈ 𝑆 ) )
23 22 ralbii ⊢ ( ∀ 𝑧 ∈ 𝑋 ∀ 𝑥 ∈ 𝑋 ( ( 𝑧 + 𝑥 ) ∈ 𝑆 → ( 𝑥 + 𝑧 ) ∈ 𝑆 ) ↔ ∀ 𝑧 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑧 + 𝑦 ) ∈ 𝑆 → ( 𝑦 + 𝑧 ) ∈ 𝑆 ) )
24 oveq1 ⊢ ( 𝑧 = 𝑥 → ( 𝑧 + 𝑦 ) = ( 𝑥 + 𝑦 ) )
25 24 eleq1d ⊢ ( 𝑧 = 𝑥 → ( ( 𝑧 + 𝑦 ) ∈ 𝑆 ↔ ( 𝑥 + 𝑦 ) ∈ 𝑆 ) )
26 oveq2 ⊢ ( 𝑧 = 𝑥 → ( 𝑦 + 𝑧 ) = ( 𝑦 + 𝑥 ) )
27 26 eleq1d ⊢ ( 𝑧 = 𝑥 → ( ( 𝑦 + 𝑧 ) ∈ 𝑆 ↔ ( 𝑦 + 𝑥 ) ∈ 𝑆 ) )
28 25 27 imbi12d ⊢ ( 𝑧 = 𝑥 → ( ( ( 𝑧 + 𝑦 ) ∈ 𝑆 → ( 𝑦 + 𝑧 ) ∈ 𝑆 ) ↔ ( ( 𝑥 + 𝑦 ) ∈ 𝑆 → ( 𝑦 + 𝑥 ) ∈ 𝑆 ) ) )
29 28 ralbidv ⊢ ( 𝑧 = 𝑥 → ( ∀ 𝑦 ∈ 𝑋 ( ( 𝑧 + 𝑦 ) ∈ 𝑆 → ( 𝑦 + 𝑧 ) ∈ 𝑆 ) ↔ ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 + 𝑦 ) ∈ 𝑆 → ( 𝑦 + 𝑥 ) ∈ 𝑆 ) ) )
30 29 cbvralvw ⊢ ( ∀ 𝑧 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑧 + 𝑦 ) ∈ 𝑆 → ( 𝑦 + 𝑧 ) ∈ 𝑆 ) ↔ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 + 𝑦 ) ∈ 𝑆 → ( 𝑦 + 𝑥 ) ∈ 𝑆 ) )
31 16 23 30 3bitri ⊢ ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( 𝑧 + 𝑥 ) ∈ 𝑆 → ( 𝑥 + 𝑧 ) ∈ 𝑆 ) ↔ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 + 𝑦 ) ∈ 𝑆 → ( 𝑦 + 𝑥 ) ∈ 𝑆 ) )
32 15 31 anbi12i ⊢ ( ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( 𝑥 + 𝑧 ) ∈ 𝑆 → ( 𝑧 + 𝑥 ) ∈ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( 𝑧 + 𝑥 ) ∈ 𝑆 → ( 𝑥 + 𝑧 ) ∈ 𝑆 ) ) ↔ ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 + 𝑦 ) ∈ 𝑆 → ( 𝑦 + 𝑥 ) ∈ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 + 𝑦 ) ∈ 𝑆 → ( 𝑦 + 𝑥 ) ∈ 𝑆 ) ) )
33 anidm ⊢ ( ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 + 𝑦 ) ∈ 𝑆 → ( 𝑦 + 𝑥 ) ∈ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 + 𝑦 ) ∈ 𝑆 → ( 𝑦 + 𝑥 ) ∈ 𝑆 ) ) ↔ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 + 𝑦 ) ∈ 𝑆 → ( 𝑦 + 𝑥 ) ∈ 𝑆 ) )
34 8 32 33 3bitri ⊢ ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( 𝑥 + 𝑧 ) ∈ 𝑆 ↔ ( 𝑧 + 𝑥 ) ∈ 𝑆 ) ↔ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 + 𝑦 ) ∈ 𝑆 → ( 𝑦 + 𝑥 ) ∈ 𝑆 ) )
35 34 anbi2i ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( 𝑥 + 𝑧 ) ∈ 𝑆 ↔ ( 𝑧 + 𝑥 ) ∈ 𝑆 ) ) ↔ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 + 𝑦 ) ∈ 𝑆 → ( 𝑦 + 𝑥 ) ∈ 𝑆 ) ) )
36 3 35 bitri ⊢ ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ↔ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 + 𝑦 ) ∈ 𝑆 → ( 𝑦 + 𝑥 ) ∈ 𝑆 ) ) )