Step |
Hyp |
Ref |
Expression |
1 |
|
spansnsh |
|- ( A e. ~H -> ( span ` { A } ) e. SH ) |
2 |
1
|
adantr |
|- ( ( A e. ~H /\ ( A +h B ) e. ( span ` { A } ) ) -> ( span ` { A } ) e. SH ) |
3 |
|
simpr |
|- ( ( A e. ~H /\ ( A +h B ) e. ( span ` { A } ) ) -> ( A +h B ) e. ( span ` { A } ) ) |
4 |
|
spansnid |
|- ( A e. ~H -> A e. ( span ` { A } ) ) |
5 |
4
|
adantr |
|- ( ( A e. ~H /\ ( A +h B ) e. ( span ` { A } ) ) -> A e. ( span ` { A } ) ) |
6 |
|
shsubcl |
|- ( ( ( span ` { A } ) e. SH /\ ( A +h B ) e. ( span ` { A } ) /\ A e. ( span ` { A } ) ) -> ( ( A +h B ) -h A ) e. ( span ` { A } ) ) |
7 |
2 3 5 6
|
syl3anc |
|- ( ( A e. ~H /\ ( A +h B ) e. ( span ` { A } ) ) -> ( ( A +h B ) -h A ) e. ( span ` { A } ) ) |
8 |
7
|
ex |
|- ( A e. ~H -> ( ( A +h B ) e. ( span ` { A } ) -> ( ( A +h B ) -h A ) e. ( span ` { A } ) ) ) |
9 |
8
|
adantr |
|- ( ( A e. ~H /\ B e. ~H ) -> ( ( A +h B ) e. ( span ` { A } ) -> ( ( A +h B ) -h A ) e. ( span ` { A } ) ) ) |
10 |
|
hvpncan2 |
|- ( ( A e. ~H /\ B e. ~H ) -> ( ( A +h B ) -h A ) = B ) |
11 |
10
|
eleq1d |
|- ( ( A e. ~H /\ B e. ~H ) -> ( ( ( A +h B ) -h A ) e. ( span ` { A } ) <-> B e. ( span ` { A } ) ) ) |
12 |
9 11
|
sylibd |
|- ( ( A e. ~H /\ B e. ~H ) -> ( ( A +h B ) e. ( span ` { A } ) -> B e. ( span ` { A } ) ) ) |
13 |
|
shaddcl |
|- ( ( ( span ` { A } ) e. SH /\ A e. ( span ` { A } ) /\ B e. ( span ` { A } ) ) -> ( A +h B ) e. ( span ` { A } ) ) |
14 |
13
|
3expia |
|- ( ( ( span ` { A } ) e. SH /\ A e. ( span ` { A } ) ) -> ( B e. ( span ` { A } ) -> ( A +h B ) e. ( span ` { A } ) ) ) |
15 |
1 4 14
|
syl2anc |
|- ( A e. ~H -> ( B e. ( span ` { A } ) -> ( A +h B ) e. ( span ` { A } ) ) ) |
16 |
15
|
adantr |
|- ( ( A e. ~H /\ B e. ~H ) -> ( B e. ( span ` { A } ) -> ( A +h B ) e. ( span ` { A } ) ) ) |
17 |
12 16
|
impbid |
|- ( ( A e. ~H /\ B e. ~H ) -> ( ( A +h B ) e. ( span ` { A } ) <-> B e. ( span ` { A } ) ) ) |