Metamath Proof Explorer

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 ⁡ G
lssnle.t ⊢ φ → T ∈ SubGrp ⁡ G
lssnle.u ⊢ φ → U ∈ SubGrp ⁡ G
Assertion lssnle ⊢ φ → ¬ U ⊆ T ↔ T ⊂ T ⊕ ˙ U

Proof

Step Hyp Ref Expression
1 lssnle.p ⊢ ⊕ ˙ = LSSum ⁡ G
2 lssnle.t ⊢ φ → T ∈ SubGrp ⁡ G
3 lssnle.u ⊢ φ → U ∈ SubGrp ⁡ G
4 1 lsmss2b ⊢ T ∈ SubGrp ⁡ G ∧ U ∈ SubGrp ⁡ G → U ⊆ T ↔ T ⊕ ˙ U = T
5 2 3 4 syl2anc ⊢ φ → U ⊆ T ↔ T ⊕ ˙ U = T
6 eqcom ⊢ T ⊕ ˙ U = T ↔ T = T ⊕ ˙ U
7 5 6 bitrdi ⊢ φ → U ⊆ T ↔ T = T ⊕ ˙ U
8 7 necon3bbid ⊢ φ → ¬ U ⊆ T ↔ T ≠ T ⊕ ˙ U
9 1 lsmub1 ⊢ T ∈ SubGrp ⁡ G ∧ U ∈ SubGrp ⁡ G → T ⊆ T ⊕ ˙ U
10 2 3 9 syl2anc ⊢ φ → T ⊆ T ⊕ ˙ U
11 df-pss ⊢ T ⊂ T ⊕ ˙ U ↔ T ⊆ T ⊕ ˙ U ∧ T ≠ T ⊕ ˙ U
12 11 baib ⊢ T ⊆ T ⊕ ˙ U → T ⊂ T ⊕ ˙ U ↔ T ≠ T ⊕ ˙ U
13 10 12 syl ⊢ φ → T ⊂ T ⊕ ˙ U ↔ T ≠ T ⊕ ˙ U
14 8 13 bitr4d ⊢ φ → ¬ U ⊆ T ↔ T ⊂ T ⊕ ˙ U