Theorem stm1addi

Description: Sum of states whose meet is 1. (Contributed by NM, 11-Nov-1999) (New usage is discouraged.)

	Ref	Expression
Hypotheses	stle.1	⊢ 𝐴 ∈ Cℋ
	stle.2	⊢ 𝐵 ∈ Cℋ
Assertion	stm1addi	⊢ ( 𝑆 ∈ States → ( ( 𝑆 ‘ ( 𝐴 ∩ 𝐵 ) ) = 1 → ( ( 𝑆 ‘ 𝐴 ) + ( 𝑆 ‘ 𝐵 ) ) = 2 ) )

Proof

Step	Hyp	Ref	Expression
1		stle.1	⊢ 𝐴 ∈ Cℋ
2		stle.2	⊢ 𝐵 ∈ Cℋ
3	1 2	stm1i	⊢ ( 𝑆 ∈ States → ( ( 𝑆 ‘ ( 𝐴 ∩ 𝐵 ) ) = 1 → ( 𝑆 ‘ 𝐴 ) = 1 ) )
4	1 2	stm1ri	⊢ ( 𝑆 ∈ States → ( ( 𝑆 ‘ ( 𝐴 ∩ 𝐵 ) ) = 1 → ( 𝑆 ‘ 𝐵 ) = 1 ) )
5	3 4	jcad	⊢ ( 𝑆 ∈ States → ( ( 𝑆 ‘ ( 𝐴 ∩ 𝐵 ) ) = 1 → ( ( 𝑆 ‘ 𝐴 ) = 1 ∧ ( 𝑆 ‘ 𝐵 ) = 1 ) ) )
6		oveq12	⊢ ( ( ( 𝑆 ‘ 𝐴 ) = 1 ∧ ( 𝑆 ‘ 𝐵 ) = 1 ) → ( ( 𝑆 ‘ 𝐴 ) + ( 𝑆 ‘ 𝐵 ) ) = ( 1 + 1 ) )
7		df-2	⊢ 2 = ( 1 + 1 )
8	6 7	eqtr4di	⊢ ( ( ( 𝑆 ‘ 𝐴 ) = 1 ∧ ( 𝑆 ‘ 𝐵 ) = 1 ) → ( ( 𝑆 ‘ 𝐴 ) + ( 𝑆 ‘ 𝐵 ) ) = 2 )
9	5 8	syl6	⊢ ( 𝑆 ∈ States → ( ( 𝑆 ‘ ( 𝐴 ∩ 𝐵 ) ) = 1 → ( ( 𝑆 ‘ 𝐴 ) + ( 𝑆 ‘ 𝐵 ) ) = 2 ) )