Metamath Proof Explorer


Theorem hstrbi

Description: Strong CH-state theorem (bidirectional version). Theorem in Mayet3 p. 10 and its converse. (Contributed by NM, 30-Jun-2006) (New usage is discouraged.)

Ref Expression
Hypotheses hstr.1 𝐴C
hstr.2 𝐵C
Assertion hstrbi ( ∀ 𝑓 ∈ CHStates ( ( norm ‘ ( 𝑓𝐴 ) ) = 1 → ( norm ‘ ( 𝑓𝐵 ) ) = 1 ) ↔ 𝐴𝐵 )

Proof

Step Hyp Ref Expression
1 hstr.1 𝐴C
2 hstr.2 𝐵C
3 1 2 hstri ( ∀ 𝑓 ∈ CHStates ( ( norm ‘ ( 𝑓𝐴 ) ) = 1 → ( norm ‘ ( 𝑓𝐵 ) ) = 1 ) → 𝐴𝐵 )
4 hstles ( ( ( 𝑓 ∈ CHStates ∧ 𝐴C ) ∧ ( 𝐵C𝐴𝐵 ) ) → ( ( norm ‘ ( 𝑓𝐴 ) ) = 1 → ( norm ‘ ( 𝑓𝐵 ) ) = 1 ) )
5 2 4 mpanr1 ( ( ( 𝑓 ∈ CHStates ∧ 𝐴C ) ∧ 𝐴𝐵 ) → ( ( norm ‘ ( 𝑓𝐴 ) ) = 1 → ( norm ‘ ( 𝑓𝐵 ) ) = 1 ) )
6 1 5 mpanl2 ( ( 𝑓 ∈ CHStates ∧ 𝐴𝐵 ) → ( ( norm ‘ ( 𝑓𝐴 ) ) = 1 → ( norm ‘ ( 𝑓𝐵 ) ) = 1 ) )
7 6 expcom ( 𝐴𝐵 → ( 𝑓 ∈ CHStates → ( ( norm ‘ ( 𝑓𝐴 ) ) = 1 → ( norm ‘ ( 𝑓𝐵 ) ) = 1 ) ) )
8 7 ralrimiv ( 𝐴𝐵 → ∀ 𝑓 ∈ CHStates ( ( norm ‘ ( 𝑓𝐴 ) ) = 1 → ( norm ‘ ( 𝑓𝐵 ) ) = 1 ) )
9 3 8 impbii ( ∀ 𝑓 ∈ CHStates ( ( norm ‘ ( 𝑓𝐴 ) ) = 1 → ( norm ‘ ( 𝑓𝐵 ) ) = 1 ) ↔ 𝐴𝐵 )