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 ) ↔ 𝐴 ⊆ 𝐵 )