Metamath Proof Explorer


Theorem hstrlem6

Description: Lemma for strong set of CH states theorem. (Contributed by NM, 30-Jun-2006) (New usage is discouraged.)

Ref Expression
Hypotheses hstrlem3.1 S = x C proj x u
hstrlem3.2 φ u A B norm u = 1
hstrlem3.3 A C
hstrlem3.4 B C
Assertion hstrlem6 φ ¬ norm S A = 1 norm S B = 1

Proof

Step Hyp Ref Expression
1 hstrlem3.1 S = x C proj x u
2 hstrlem3.2 φ u A B norm u = 1
3 hstrlem3.3 A C
4 hstrlem3.4 B C
5 1 2 3 4 hstrlem4 φ norm S A = 1
6 1 2 3 4 hstrlem3 φ S CHStates
7 hstcl S CHStates B C S B
8 6 4 7 sylancl φ S B
9 normcl S B norm S B
10 8 9 syl φ norm S B
11 1 2 3 4 hstrlem5 φ norm S B < 1
12 10 11 ltned φ norm S B 1
13 12 neneqd φ ¬ norm S B = 1
14 5 13 jcnd φ ¬ norm S A = 1 norm S B = 1