Theorem lssnle

Description: Equivalent expressions for "not less than". ( chnlei analog.) (Contributed by NM, 10-Jan-2015) (Revised by Mario Carneiro, 19-Apr-2016)

	Ref	Expression
Hypotheses	lssnle.p	⊢ ⊕ = ( LSSum ‘ 𝐺 )
	lssnle.t	⊢ ( 𝜑 → 𝑇 ∈ ( SubGrp ‘ 𝐺 ) )
	lssnle.u	⊢ ( 𝜑 → 𝑈 ∈ ( SubGrp ‘ 𝐺 ) )
Assertion	lssnle	⊢ ( 𝜑 → ( ¬ 𝑈 ⊆ 𝑇 ↔ 𝑇 ⊊ ( 𝑇 ⊕ 𝑈 ) ) )

Proof

Step	Hyp	Ref	Expression
1		lssnle.p	⊢ ⊕ = ( LSSum ‘ 𝐺 )
2		lssnle.t	⊢ ( 𝜑 → 𝑇 ∈ ( SubGrp ‘ 𝐺 ) )
3		lssnle.u	⊢ ( 𝜑 → 𝑈 ∈ ( SubGrp ‘ 𝐺 ) )
4	1	lsmss2b	⊢ ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) → ( 𝑈 ⊆ 𝑇 ↔ ( 𝑇 ⊕ 𝑈 ) = 𝑇 ) )
5	2 3 4	syl2anc	⊢ ( 𝜑 → ( 𝑈 ⊆ 𝑇 ↔ ( 𝑇 ⊕ 𝑈 ) = 𝑇 ) )
6		eqcom	⊢ ( ( 𝑇 ⊕ 𝑈 ) = 𝑇 ↔ 𝑇 = ( 𝑇 ⊕ 𝑈 ) )
7	5 6	bitrdi	⊢ ( 𝜑 → ( 𝑈 ⊆ 𝑇 ↔ 𝑇 = ( 𝑇 ⊕ 𝑈 ) ) )
8	7	necon3bbid	⊢ ( 𝜑 → ( ¬ 𝑈 ⊆ 𝑇 ↔ 𝑇 ≠ ( 𝑇 ⊕ 𝑈 ) ) )
9	1	lsmub1	⊢ ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) → 𝑇 ⊆ ( 𝑇 ⊕ 𝑈 ) )
10	2 3 9	syl2anc	⊢ ( 𝜑 → 𝑇 ⊆ ( 𝑇 ⊕ 𝑈 ) )
11		df-pss	⊢ ( 𝑇 ⊊ ( 𝑇 ⊕ 𝑈 ) ↔ ( 𝑇 ⊆ ( 𝑇 ⊕ 𝑈 ) ∧ 𝑇 ≠ ( 𝑇 ⊕ 𝑈 ) ) )
12	11	baib	⊢ ( 𝑇 ⊆ ( 𝑇 ⊕ 𝑈 ) → ( 𝑇 ⊊ ( 𝑇 ⊕ 𝑈 ) ↔ 𝑇 ≠ ( 𝑇 ⊕ 𝑈 ) ) )
13	10 12	syl	⊢ ( 𝜑 → ( 𝑇 ⊊ ( 𝑇 ⊕ 𝑈 ) ↔ 𝑇 ≠ ( 𝑇 ⊕ 𝑈 ) ) )
14	8 13	bitr4d	⊢ ( 𝜑 → ( ¬ 𝑈 ⊆ 𝑇 ↔ 𝑇 ⊊ ( 𝑇 ⊕ 𝑈 ) ) )