This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem atcv1

Description: Two atoms covering the zero subspace are equal. (Contributed by NM, 26-Jun-2004) (New usage is discouraged.)

Ref Expression
Assertion atcv1 ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) ∧ 𝐴 ⋖ℋ ( 𝐵 ∨ℋ 𝐶 ) ) → ( 𝐴 = 0ℋ ↔ 𝐵 = 𝐶 ) )

Proof

Step Hyp Ref Expression
1 breq1 ⊢ ( 𝐴 = 0ℋ → ( 𝐴 ⋖ℋ ( 𝐵 ∨ℋ 𝐶 ) ↔ 0ℋ ⋖ℋ ( 𝐵 ∨ℋ 𝐶 ) ) )
2 atcv0eq ⊢ ( ( 𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) → ( 0ℋ ⋖ℋ ( 𝐵 ∨ℋ 𝐶 ) ↔ 𝐵 = 𝐶 ) )
3 1 2 sylan9bbr ⊢ ( ( ( 𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) ∧ 𝐴 = 0ℋ ) → ( 𝐴 ⋖ℋ ( 𝐵 ∨ℋ 𝐶 ) ↔ 𝐵 = 𝐶 ) )
4 3 biimpd ⊢ ( ( ( 𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) ∧ 𝐴 = 0ℋ ) → ( 𝐴 ⋖ℋ ( 𝐵 ∨ℋ 𝐶 ) → 𝐵 = 𝐶 ) )
5 4 ex ⊢ ( ( 𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) → ( 𝐴 = 0ℋ → ( 𝐴 ⋖ℋ ( 𝐵 ∨ℋ 𝐶 ) → 𝐵 = 𝐶 ) ) )
6 5 com23 ⊢ ( ( 𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) → ( 𝐴 ⋖ℋ ( 𝐵 ∨ℋ 𝐶 ) → ( 𝐴 = 0ℋ → 𝐵 = 𝐶 ) ) )
7 6 3adant1 ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) → ( 𝐴 ⋖ℋ ( 𝐵 ∨ℋ 𝐶 ) → ( 𝐴 = 0ℋ → 𝐵 = 𝐶 ) ) )
8 7 imp ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) ∧ 𝐴 ⋖ℋ ( 𝐵 ∨ℋ 𝐶 ) ) → ( 𝐴 = 0ℋ → 𝐵 = 𝐶 ) )
9 oveq1 ⊢ ( 𝐵 = 𝐶 → ( 𝐵 ∨ℋ 𝐶 ) = ( 𝐶 ∨ℋ 𝐶 ) )
10 atelch ⊢ ( 𝐶 ∈ HAtoms → 𝐶 ∈ Cℋ )
11 chjidm ⊢ ( 𝐶 ∈ Cℋ → ( 𝐶 ∨ℋ 𝐶 ) = 𝐶 )
12 10 11 syl ⊢ ( 𝐶 ∈ HAtoms → ( 𝐶 ∨ℋ 𝐶 ) = 𝐶 )
13 9 12 sylan9eq ⊢ ( ( 𝐵 = 𝐶 ∧ 𝐶 ∈ HAtoms ) → ( 𝐵 ∨ℋ 𝐶 ) = 𝐶 )
14 13 eqcomd ⊢ ( ( 𝐵 = 𝐶 ∧ 𝐶 ∈ HAtoms ) → 𝐶 = ( 𝐵 ∨ℋ 𝐶 ) )
15 14 eleq1d ⊢ ( ( 𝐵 = 𝐶 ∧ 𝐶 ∈ HAtoms ) → ( 𝐶 ∈ HAtoms ↔ ( 𝐵 ∨ℋ 𝐶 ) ∈ HAtoms ) )
16 15 ex ⊢ ( 𝐵 = 𝐶 → ( 𝐶 ∈ HAtoms → ( 𝐶 ∈ HAtoms ↔ ( 𝐵 ∨ℋ 𝐶 ) ∈ HAtoms ) ) )
17 16 ibd ⊢ ( 𝐵 = 𝐶 → ( 𝐶 ∈ HAtoms → ( 𝐵 ∨ℋ 𝐶 ) ∈ HAtoms ) )
18 17 impcom ⊢ ( ( 𝐶 ∈ HAtoms ∧ 𝐵 = 𝐶 ) → ( 𝐵 ∨ℋ 𝐶 ) ∈ HAtoms )
19 atcveq0 ⊢ ( ( 𝐴 ∈ Cℋ ∧ ( 𝐵 ∨ℋ 𝐶 ) ∈ HAtoms ) → ( 𝐴 ⋖ℋ ( 𝐵 ∨ℋ 𝐶 ) ↔ 𝐴 = 0ℋ ) )
20 18 19 sylan2 ⊢ ( ( 𝐴 ∈ Cℋ ∧ ( 𝐶 ∈ HAtoms ∧ 𝐵 = 𝐶 ) ) → ( 𝐴 ⋖ℋ ( 𝐵 ∨ℋ 𝐶 ) ↔ 𝐴 = 0ℋ ) )
21 20 biimpd ⊢ ( ( 𝐴 ∈ Cℋ ∧ ( 𝐶 ∈ HAtoms ∧ 𝐵 = 𝐶 ) ) → ( 𝐴 ⋖ℋ ( 𝐵 ∨ℋ 𝐶 ) → 𝐴 = 0ℋ ) )
22 21 exp32 ⊢ ( 𝐴 ∈ Cℋ → ( 𝐶 ∈ HAtoms → ( 𝐵 = 𝐶 → ( 𝐴 ⋖ℋ ( 𝐵 ∨ℋ 𝐶 ) → 𝐴 = 0ℋ ) ) ) )
23 22 com34 ⊢ ( 𝐴 ∈ Cℋ → ( 𝐶 ∈ HAtoms → ( 𝐴 ⋖ℋ ( 𝐵 ∨ℋ 𝐶 ) → ( 𝐵 = 𝐶 → 𝐴 = 0ℋ ) ) ) )
24 23 imp ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐶 ∈ HAtoms ) → ( 𝐴 ⋖ℋ ( 𝐵 ∨ℋ 𝐶 ) → ( 𝐵 = 𝐶 → 𝐴 = 0ℋ ) ) )
25 24 3adant2 ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) → ( 𝐴 ⋖ℋ ( 𝐵 ∨ℋ 𝐶 ) → ( 𝐵 = 𝐶 → 𝐴 = 0ℋ ) ) )
26 25 imp ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) ∧ 𝐴 ⋖ℋ ( 𝐵 ∨ℋ 𝐶 ) ) → ( 𝐵 = 𝐶 → 𝐴 = 0ℋ ) )
27 8 26 impbid ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) ∧ 𝐴 ⋖ℋ ( 𝐵 ∨ℋ 𝐶 ) ) → ( 𝐴 = 0ℋ ↔ 𝐵 = 𝐶 ) )