Theorem isgrpix

Description: Properties that determine a group. Read N as N ( x ) . Note: This theorem has hard-coded structure indices for demonstration purposes. It is not intended for general use. (New usage is discouraged.) (Contributed by NM, 4-Sep-2011)

	Ref	Expression
Hypotheses	isgrpix.a	⊢ 𝐵 ∈ V
	isgrpix.b	⊢ + ∈ V
	isgrpix.g	⊢ 𝐺 = { ⟨ 1 , 𝐵 ⟩ , ⟨ 2 , + ⟩ }
	isgrpix.2	⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 + 𝑦 ) ∈ 𝐵 )
	isgrpix.3	⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) → ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( 𝑥 + ( 𝑦 + 𝑧 ) ) )
	isgrpix.z	⊢ 0 ∈ 𝐵
	isgrpix.5	⊢ ( 𝑥 ∈ 𝐵 → ( 0 + 𝑥 ) = 𝑥 )
	isgrpix.6	⊢ ( 𝑥 ∈ 𝐵 → 𝑁 ∈ 𝐵 )
	isgrpix.7	⊢ ( 𝑥 ∈ 𝐵 → ( 𝑁 + 𝑥 ) = 0 )
Assertion	isgrpix	⊢ 𝐺 ∈ Grp

Proof

Step	Hyp	Ref	Expression
1		isgrpix.a	⊢ 𝐵 ∈ V
2		isgrpix.b	⊢ + ∈ V
3		isgrpix.g	⊢ 𝐺 = { ⟨ 1 , 𝐵 ⟩ , ⟨ 2 , + ⟩ }
4		isgrpix.2	⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 + 𝑦 ) ∈ 𝐵 )
5		isgrpix.3	⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) → ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( 𝑥 + ( 𝑦 + 𝑧 ) ) )
6		isgrpix.z	⊢ 0 ∈ 𝐵
7		isgrpix.5	⊢ ( 𝑥 ∈ 𝐵 → ( 0 + 𝑥 ) = 𝑥 )
8		isgrpix.6	⊢ ( 𝑥 ∈ 𝐵 → 𝑁 ∈ 𝐵 )
9		isgrpix.7	⊢ ( 𝑥 ∈ 𝐵 → ( 𝑁 + 𝑥 ) = 0 )
10	1 2 3	grpbasex	⊢ 𝐵 = ( Base ‘ 𝐺 )
11	1 2 3	grpplusgx	⊢ + = ( +g ‘ 𝐺 )
12	10 11 4 5 6 7 8 9	isgrpi	⊢ 𝐺 ∈ Grp