Metamath Proof Explorer


Theorem superpos

Description: Superposition Principle. If A and B are distinct atoms, there exists a third atom, distinct from A and B , that is the superposition of A and B . Definition 3.4-3(a) in MegPav2000 p. 2345 (PDF p. 8). (Contributed by NM, 9-Jun-2006) (New usage is discouraged.)

Ref Expression
Assertion superpos ( ( ๐ด โˆˆ HAtoms โˆง ๐ต โˆˆ HAtoms โˆง ๐ด โ‰  ๐ต ) โ†’ โˆƒ ๐‘ฅ โˆˆ HAtoms ( ๐‘ฅ โ‰  ๐ด โˆง ๐‘ฅ โ‰  ๐ต โˆง ๐‘ฅ โŠ† ( ๐ด โˆจโ„‹ ๐ต ) ) )

Proof

Step Hyp Ref Expression
1 atom1d โŠข ( ๐ด โˆˆ HAtoms โ†” โˆƒ ๐‘ฆ โˆˆ โ„‹ ( ๐‘ฆ โ‰  0โ„Ž โˆง ๐ด = ( span โ€˜ { ๐‘ฆ } ) ) )
2 atom1d โŠข ( ๐ต โˆˆ HAtoms โ†” โˆƒ ๐‘ง โˆˆ โ„‹ ( ๐‘ง โ‰  0โ„Ž โˆง ๐ต = ( span โ€˜ { ๐‘ง } ) ) )
3 reeanv โŠข ( โˆƒ ๐‘ฆ โˆˆ โ„‹ โˆƒ ๐‘ง โˆˆ โ„‹ ( ( ๐‘ฆ โ‰  0โ„Ž โˆง ๐ด = ( span โ€˜ { ๐‘ฆ } ) ) โˆง ( ๐‘ง โ‰  0โ„Ž โˆง ๐ต = ( span โ€˜ { ๐‘ง } ) ) ) โ†” ( โˆƒ ๐‘ฆ โˆˆ โ„‹ ( ๐‘ฆ โ‰  0โ„Ž โˆง ๐ด = ( span โ€˜ { ๐‘ฆ } ) ) โˆง โˆƒ ๐‘ง โˆˆ โ„‹ ( ๐‘ง โ‰  0โ„Ž โˆง ๐ต = ( span โ€˜ { ๐‘ง } ) ) ) )
4 an4 โŠข ( ( ( ๐‘ฆ โ‰  0โ„Ž โˆง ๐ด = ( span โ€˜ { ๐‘ฆ } ) ) โˆง ( ๐‘ง โ‰  0โ„Ž โˆง ๐ต = ( span โ€˜ { ๐‘ง } ) ) ) โ†” ( ( ๐‘ฆ โ‰  0โ„Ž โˆง ๐‘ง โ‰  0โ„Ž ) โˆง ( ๐ด = ( span โ€˜ { ๐‘ฆ } ) โˆง ๐ต = ( span โ€˜ { ๐‘ง } ) ) ) )
5 neeq1 โŠข ( ๐ด = ( span โ€˜ { ๐‘ฆ } ) โ†’ ( ๐ด โ‰  ๐ต โ†” ( span โ€˜ { ๐‘ฆ } ) โ‰  ๐ต ) )
6 neeq2 โŠข ( ๐ต = ( span โ€˜ { ๐‘ง } ) โ†’ ( ( span โ€˜ { ๐‘ฆ } ) โ‰  ๐ต โ†” ( span โ€˜ { ๐‘ฆ } ) โ‰  ( span โ€˜ { ๐‘ง } ) ) )
7 5 6 sylan9bb โŠข ( ( ๐ด = ( span โ€˜ { ๐‘ฆ } ) โˆง ๐ต = ( span โ€˜ { ๐‘ง } ) ) โ†’ ( ๐ด โ‰  ๐ต โ†” ( span โ€˜ { ๐‘ฆ } ) โ‰  ( span โ€˜ { ๐‘ง } ) ) )
8 7 adantl โŠข ( ( ( ( ๐‘ฆ โˆˆ โ„‹ โˆง ๐‘ง โˆˆ โ„‹ ) โˆง ( ๐‘ฆ โ‰  0โ„Ž โˆง ๐‘ง โ‰  0โ„Ž ) ) โˆง ( ๐ด = ( span โ€˜ { ๐‘ฆ } ) โˆง ๐ต = ( span โ€˜ { ๐‘ง } ) ) ) โ†’ ( ๐ด โ‰  ๐ต โ†” ( span โ€˜ { ๐‘ฆ } ) โ‰  ( span โ€˜ { ๐‘ง } ) ) )
9 hvaddcl โŠข ( ( ๐‘ฆ โˆˆ โ„‹ โˆง ๐‘ง โˆˆ โ„‹ ) โ†’ ( ๐‘ฆ +โ„Ž ๐‘ง ) โˆˆ โ„‹ )
10 9 adantr โŠข ( ( ( ๐‘ฆ โˆˆ โ„‹ โˆง ๐‘ง โˆˆ โ„‹ ) โˆง ( span โ€˜ { ๐‘ฆ } ) โ‰  ( span โ€˜ { ๐‘ง } ) ) โ†’ ( ๐‘ฆ +โ„Ž ๐‘ง ) โˆˆ โ„‹ )
11 hvaddeq0 โŠข ( ( ๐‘ฆ โˆˆ โ„‹ โˆง ๐‘ง โˆˆ โ„‹ ) โ†’ ( ( ๐‘ฆ +โ„Ž ๐‘ง ) = 0โ„Ž โ†” ๐‘ฆ = ( - 1 ยทโ„Ž ๐‘ง ) ) )
12 sneq โŠข ( ๐‘ฆ = ( - 1 ยทโ„Ž ๐‘ง ) โ†’ { ๐‘ฆ } = { ( - 1 ยทโ„Ž ๐‘ง ) } )
13 12 fveq2d โŠข ( ๐‘ฆ = ( - 1 ยทโ„Ž ๐‘ง ) โ†’ ( span โ€˜ { ๐‘ฆ } ) = ( span โ€˜ { ( - 1 ยทโ„Ž ๐‘ง ) } ) )
14 neg1cn โŠข - 1 โˆˆ โ„‚
15 neg1ne0 โŠข - 1 โ‰  0
16 spansncol โŠข ( ( ๐‘ง โˆˆ โ„‹ โˆง - 1 โˆˆ โ„‚ โˆง - 1 โ‰  0 ) โ†’ ( span โ€˜ { ( - 1 ยทโ„Ž ๐‘ง ) } ) = ( span โ€˜ { ๐‘ง } ) )
17 14 15 16 mp3an23 โŠข ( ๐‘ง โˆˆ โ„‹ โ†’ ( span โ€˜ { ( - 1 ยทโ„Ž ๐‘ง ) } ) = ( span โ€˜ { ๐‘ง } ) )
18 13 17 sylan9eqr โŠข ( ( ๐‘ง โˆˆ โ„‹ โˆง ๐‘ฆ = ( - 1 ยทโ„Ž ๐‘ง ) ) โ†’ ( span โ€˜ { ๐‘ฆ } ) = ( span โ€˜ { ๐‘ง } ) )
19 18 ex โŠข ( ๐‘ง โˆˆ โ„‹ โ†’ ( ๐‘ฆ = ( - 1 ยทโ„Ž ๐‘ง ) โ†’ ( span โ€˜ { ๐‘ฆ } ) = ( span โ€˜ { ๐‘ง } ) ) )
20 19 adantl โŠข ( ( ๐‘ฆ โˆˆ โ„‹ โˆง ๐‘ง โˆˆ โ„‹ ) โ†’ ( ๐‘ฆ = ( - 1 ยทโ„Ž ๐‘ง ) โ†’ ( span โ€˜ { ๐‘ฆ } ) = ( span โ€˜ { ๐‘ง } ) ) )
21 11 20 sylbid โŠข ( ( ๐‘ฆ โˆˆ โ„‹ โˆง ๐‘ง โˆˆ โ„‹ ) โ†’ ( ( ๐‘ฆ +โ„Ž ๐‘ง ) = 0โ„Ž โ†’ ( span โ€˜ { ๐‘ฆ } ) = ( span โ€˜ { ๐‘ง } ) ) )
22 21 necon3d โŠข ( ( ๐‘ฆ โˆˆ โ„‹ โˆง ๐‘ง โˆˆ โ„‹ ) โ†’ ( ( span โ€˜ { ๐‘ฆ } ) โ‰  ( span โ€˜ { ๐‘ง } ) โ†’ ( ๐‘ฆ +โ„Ž ๐‘ง ) โ‰  0โ„Ž ) )
23 22 imp โŠข ( ( ( ๐‘ฆ โˆˆ โ„‹ โˆง ๐‘ง โˆˆ โ„‹ ) โˆง ( span โ€˜ { ๐‘ฆ } ) โ‰  ( span โ€˜ { ๐‘ง } ) ) โ†’ ( ๐‘ฆ +โ„Ž ๐‘ง ) โ‰  0โ„Ž )
24 spansna โŠข ( ( ( ๐‘ฆ +โ„Ž ๐‘ง ) โˆˆ โ„‹ โˆง ( ๐‘ฆ +โ„Ž ๐‘ง ) โ‰  0โ„Ž ) โ†’ ( span โ€˜ { ( ๐‘ฆ +โ„Ž ๐‘ง ) } ) โˆˆ HAtoms )
25 10 23 24 syl2anc โŠข ( ( ( ๐‘ฆ โˆˆ โ„‹ โˆง ๐‘ง โˆˆ โ„‹ ) โˆง ( span โ€˜ { ๐‘ฆ } ) โ‰  ( span โ€˜ { ๐‘ง } ) ) โ†’ ( span โ€˜ { ( ๐‘ฆ +โ„Ž ๐‘ง ) } ) โˆˆ HAtoms )
26 25 adantlr โŠข ( ( ( ( ๐‘ฆ โˆˆ โ„‹ โˆง ๐‘ง โˆˆ โ„‹ ) โˆง ( ๐‘ฆ โ‰  0โ„Ž โˆง ๐‘ง โ‰  0โ„Ž ) ) โˆง ( span โ€˜ { ๐‘ฆ } ) โ‰  ( span โ€˜ { ๐‘ง } ) ) โ†’ ( span โ€˜ { ( ๐‘ฆ +โ„Ž ๐‘ง ) } ) โˆˆ HAtoms )
27 26 adantlr โŠข ( ( ( ( ( ๐‘ฆ โˆˆ โ„‹ โˆง ๐‘ง โˆˆ โ„‹ ) โˆง ( ๐‘ฆ โ‰  0โ„Ž โˆง ๐‘ง โ‰  0โ„Ž ) ) โˆง ( ๐ด = ( span โ€˜ { ๐‘ฆ } ) โˆง ๐ต = ( span โ€˜ { ๐‘ง } ) ) ) โˆง ( span โ€˜ { ๐‘ฆ } ) โ‰  ( span โ€˜ { ๐‘ง } ) ) โ†’ ( span โ€˜ { ( ๐‘ฆ +โ„Ž ๐‘ง ) } ) โˆˆ HAtoms )
28 eqeq2 โŠข ( ๐ด = ( span โ€˜ { ๐‘ฆ } ) โ†’ ( ( span โ€˜ { ( ๐‘ฆ +โ„Ž ๐‘ง ) } ) = ๐ด โ†” ( span โ€˜ { ( ๐‘ฆ +โ„Ž ๐‘ง ) } ) = ( span โ€˜ { ๐‘ฆ } ) ) )
29 28 biimpd โŠข ( ๐ด = ( span โ€˜ { ๐‘ฆ } ) โ†’ ( ( span โ€˜ { ( ๐‘ฆ +โ„Ž ๐‘ง ) } ) = ๐ด โ†’ ( span โ€˜ { ( ๐‘ฆ +โ„Ž ๐‘ง ) } ) = ( span โ€˜ { ๐‘ฆ } ) ) )
30 spansneleqi โŠข ( ( ๐‘ฆ +โ„Ž ๐‘ง ) โˆˆ โ„‹ โ†’ ( ( span โ€˜ { ( ๐‘ฆ +โ„Ž ๐‘ง ) } ) = ( span โ€˜ { ๐‘ฆ } ) โ†’ ( ๐‘ฆ +โ„Ž ๐‘ง ) โˆˆ ( span โ€˜ { ๐‘ฆ } ) ) )
31 9 30 syl โŠข ( ( ๐‘ฆ โˆˆ โ„‹ โˆง ๐‘ง โˆˆ โ„‹ ) โ†’ ( ( span โ€˜ { ( ๐‘ฆ +โ„Ž ๐‘ง ) } ) = ( span โ€˜ { ๐‘ฆ } ) โ†’ ( ๐‘ฆ +โ„Ž ๐‘ง ) โˆˆ ( span โ€˜ { ๐‘ฆ } ) ) )
32 elspansn โŠข ( ๐‘ฆ โˆˆ โ„‹ โ†’ ( ( ๐‘ฆ +โ„Ž ๐‘ง ) โˆˆ ( span โ€˜ { ๐‘ฆ } ) โ†” โˆƒ ๐‘ฃ โˆˆ โ„‚ ( ๐‘ฆ +โ„Ž ๐‘ง ) = ( ๐‘ฃ ยทโ„Ž ๐‘ฆ ) ) )
33 32 adantr โŠข ( ( ๐‘ฆ โˆˆ โ„‹ โˆง ๐‘ง โˆˆ โ„‹ ) โ†’ ( ( ๐‘ฆ +โ„Ž ๐‘ง ) โˆˆ ( span โ€˜ { ๐‘ฆ } ) โ†” โˆƒ ๐‘ฃ โˆˆ โ„‚ ( ๐‘ฆ +โ„Ž ๐‘ง ) = ( ๐‘ฃ ยทโ„Ž ๐‘ฆ ) ) )
34 addcl โŠข ( ( ๐‘ฃ โˆˆ โ„‚ โˆง - 1 โˆˆ โ„‚ ) โ†’ ( ๐‘ฃ + - 1 ) โˆˆ โ„‚ )
35 14 34 mpan2 โŠข ( ๐‘ฃ โˆˆ โ„‚ โ†’ ( ๐‘ฃ + - 1 ) โˆˆ โ„‚ )
36 35 ad2antlr โŠข ( ( ( ( ๐‘ฆ โˆˆ โ„‹ โˆง ๐‘ง โˆˆ โ„‹ ) โˆง ๐‘ฃ โˆˆ โ„‚ ) โˆง ( ๐‘ฆ +โ„Ž ๐‘ง ) = ( ๐‘ฃ ยทโ„Ž ๐‘ฆ ) ) โ†’ ( ๐‘ฃ + - 1 ) โˆˆ โ„‚ )
37 hvmulcl โŠข ( ( ๐‘ฃ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‹ ) โ†’ ( ๐‘ฃ ยทโ„Ž ๐‘ฆ ) โˆˆ โ„‹ )
38 37 ancoms โŠข ( ( ๐‘ฆ โˆˆ โ„‹ โˆง ๐‘ฃ โˆˆ โ„‚ ) โ†’ ( ๐‘ฃ ยทโ„Ž ๐‘ฆ ) โˆˆ โ„‹ )
39 38 adantlr โŠข ( ( ( ๐‘ฆ โˆˆ โ„‹ โˆง ๐‘ง โˆˆ โ„‹ ) โˆง ๐‘ฃ โˆˆ โ„‚ ) โ†’ ( ๐‘ฃ ยทโ„Ž ๐‘ฆ ) โˆˆ โ„‹ )
40 simpll โŠข ( ( ( ๐‘ฆ โˆˆ โ„‹ โˆง ๐‘ง โˆˆ โ„‹ ) โˆง ๐‘ฃ โˆˆ โ„‚ ) โ†’ ๐‘ฆ โˆˆ โ„‹ )
41 simplr โŠข ( ( ( ๐‘ฆ โˆˆ โ„‹ โˆง ๐‘ง โˆˆ โ„‹ ) โˆง ๐‘ฃ โˆˆ โ„‚ ) โ†’ ๐‘ง โˆˆ โ„‹ )
42 hvsubadd โŠข ( ( ( ๐‘ฃ ยทโ„Ž ๐‘ฆ ) โˆˆ โ„‹ โˆง ๐‘ฆ โˆˆ โ„‹ โˆง ๐‘ง โˆˆ โ„‹ ) โ†’ ( ( ( ๐‘ฃ ยทโ„Ž ๐‘ฆ ) โˆ’โ„Ž ๐‘ฆ ) = ๐‘ง โ†” ( ๐‘ฆ +โ„Ž ๐‘ง ) = ( ๐‘ฃ ยทโ„Ž ๐‘ฆ ) ) )
43 39 40 41 42 syl3anc โŠข ( ( ( ๐‘ฆ โˆˆ โ„‹ โˆง ๐‘ง โˆˆ โ„‹ ) โˆง ๐‘ฃ โˆˆ โ„‚ ) โ†’ ( ( ( ๐‘ฃ ยทโ„Ž ๐‘ฆ ) โˆ’โ„Ž ๐‘ฆ ) = ๐‘ง โ†” ( ๐‘ฆ +โ„Ž ๐‘ง ) = ( ๐‘ฃ ยทโ„Ž ๐‘ฆ ) ) )
44 43 biimpar โŠข ( ( ( ( ๐‘ฆ โˆˆ โ„‹ โˆง ๐‘ง โˆˆ โ„‹ ) โˆง ๐‘ฃ โˆˆ โ„‚ ) โˆง ( ๐‘ฆ +โ„Ž ๐‘ง ) = ( ๐‘ฃ ยทโ„Ž ๐‘ฆ ) ) โ†’ ( ( ๐‘ฃ ยทโ„Ž ๐‘ฆ ) โˆ’โ„Ž ๐‘ฆ ) = ๐‘ง )
45 hvsubval โŠข ( ( ( ๐‘ฃ ยทโ„Ž ๐‘ฆ ) โˆˆ โ„‹ โˆง ๐‘ฆ โˆˆ โ„‹ ) โ†’ ( ( ๐‘ฃ ยทโ„Ž ๐‘ฆ ) โˆ’โ„Ž ๐‘ฆ ) = ( ( ๐‘ฃ ยทโ„Ž ๐‘ฆ ) +โ„Ž ( - 1 ยทโ„Ž ๐‘ฆ ) ) )
46 37 45 sylancom โŠข ( ( ๐‘ฃ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‹ ) โ†’ ( ( ๐‘ฃ ยทโ„Ž ๐‘ฆ ) โˆ’โ„Ž ๐‘ฆ ) = ( ( ๐‘ฃ ยทโ„Ž ๐‘ฆ ) +โ„Ž ( - 1 ยทโ„Ž ๐‘ฆ ) ) )
47 ax-hvdistr2 โŠข ( ( ๐‘ฃ โˆˆ โ„‚ โˆง - 1 โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‹ ) โ†’ ( ( ๐‘ฃ + - 1 ) ยทโ„Ž ๐‘ฆ ) = ( ( ๐‘ฃ ยทโ„Ž ๐‘ฆ ) +โ„Ž ( - 1 ยทโ„Ž ๐‘ฆ ) ) )
48 14 47 mp3an2 โŠข ( ( ๐‘ฃ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‹ ) โ†’ ( ( ๐‘ฃ + - 1 ) ยทโ„Ž ๐‘ฆ ) = ( ( ๐‘ฃ ยทโ„Ž ๐‘ฆ ) +โ„Ž ( - 1 ยทโ„Ž ๐‘ฆ ) ) )
49 46 48 eqtr4d โŠข ( ( ๐‘ฃ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‹ ) โ†’ ( ( ๐‘ฃ ยทโ„Ž ๐‘ฆ ) โˆ’โ„Ž ๐‘ฆ ) = ( ( ๐‘ฃ + - 1 ) ยทโ„Ž ๐‘ฆ ) )
50 49 ancoms โŠข ( ( ๐‘ฆ โˆˆ โ„‹ โˆง ๐‘ฃ โˆˆ โ„‚ ) โ†’ ( ( ๐‘ฃ ยทโ„Ž ๐‘ฆ ) โˆ’โ„Ž ๐‘ฆ ) = ( ( ๐‘ฃ + - 1 ) ยทโ„Ž ๐‘ฆ ) )
51 50 adantlr โŠข ( ( ( ๐‘ฆ โˆˆ โ„‹ โˆง ๐‘ง โˆˆ โ„‹ ) โˆง ๐‘ฃ โˆˆ โ„‚ ) โ†’ ( ( ๐‘ฃ ยทโ„Ž ๐‘ฆ ) โˆ’โ„Ž ๐‘ฆ ) = ( ( ๐‘ฃ + - 1 ) ยทโ„Ž ๐‘ฆ ) )
52 51 adantr โŠข ( ( ( ( ๐‘ฆ โˆˆ โ„‹ โˆง ๐‘ง โˆˆ โ„‹ ) โˆง ๐‘ฃ โˆˆ โ„‚ ) โˆง ( ๐‘ฆ +โ„Ž ๐‘ง ) = ( ๐‘ฃ ยทโ„Ž ๐‘ฆ ) ) โ†’ ( ( ๐‘ฃ ยทโ„Ž ๐‘ฆ ) โˆ’โ„Ž ๐‘ฆ ) = ( ( ๐‘ฃ + - 1 ) ยทโ„Ž ๐‘ฆ ) )
53 44 52 eqtr3d โŠข ( ( ( ( ๐‘ฆ โˆˆ โ„‹ โˆง ๐‘ง โˆˆ โ„‹ ) โˆง ๐‘ฃ โˆˆ โ„‚ ) โˆง ( ๐‘ฆ +โ„Ž ๐‘ง ) = ( ๐‘ฃ ยทโ„Ž ๐‘ฆ ) ) โ†’ ๐‘ง = ( ( ๐‘ฃ + - 1 ) ยทโ„Ž ๐‘ฆ ) )
54 oveq1 โŠข ( ๐‘ค = ( ๐‘ฃ + - 1 ) โ†’ ( ๐‘ค ยทโ„Ž ๐‘ฆ ) = ( ( ๐‘ฃ + - 1 ) ยทโ„Ž ๐‘ฆ ) )
55 54 rspceeqv โŠข ( ( ( ๐‘ฃ + - 1 ) โˆˆ โ„‚ โˆง ๐‘ง = ( ( ๐‘ฃ + - 1 ) ยทโ„Ž ๐‘ฆ ) ) โ†’ โˆƒ ๐‘ค โˆˆ โ„‚ ๐‘ง = ( ๐‘ค ยทโ„Ž ๐‘ฆ ) )
56 36 53 55 syl2anc โŠข ( ( ( ( ๐‘ฆ โˆˆ โ„‹ โˆง ๐‘ง โˆˆ โ„‹ ) โˆง ๐‘ฃ โˆˆ โ„‚ ) โˆง ( ๐‘ฆ +โ„Ž ๐‘ง ) = ( ๐‘ฃ ยทโ„Ž ๐‘ฆ ) ) โ†’ โˆƒ ๐‘ค โˆˆ โ„‚ ๐‘ง = ( ๐‘ค ยทโ„Ž ๐‘ฆ ) )
57 56 rexlimdva2 โŠข ( ( ๐‘ฆ โˆˆ โ„‹ โˆง ๐‘ง โˆˆ โ„‹ ) โ†’ ( โˆƒ ๐‘ฃ โˆˆ โ„‚ ( ๐‘ฆ +โ„Ž ๐‘ง ) = ( ๐‘ฃ ยทโ„Ž ๐‘ฆ ) โ†’ โˆƒ ๐‘ค โˆˆ โ„‚ ๐‘ง = ( ๐‘ค ยทโ„Ž ๐‘ฆ ) ) )
58 33 57 sylbid โŠข ( ( ๐‘ฆ โˆˆ โ„‹ โˆง ๐‘ง โˆˆ โ„‹ ) โ†’ ( ( ๐‘ฆ +โ„Ž ๐‘ง ) โˆˆ ( span โ€˜ { ๐‘ฆ } ) โ†’ โˆƒ ๐‘ค โˆˆ โ„‚ ๐‘ง = ( ๐‘ค ยทโ„Ž ๐‘ฆ ) ) )
59 31 58 syld โŠข ( ( ๐‘ฆ โˆˆ โ„‹ โˆง ๐‘ง โˆˆ โ„‹ ) โ†’ ( ( span โ€˜ { ( ๐‘ฆ +โ„Ž ๐‘ง ) } ) = ( span โ€˜ { ๐‘ฆ } ) โ†’ โˆƒ ๐‘ค โˆˆ โ„‚ ๐‘ง = ( ๐‘ค ยทโ„Ž ๐‘ฆ ) ) )
60 elspansn โŠข ( ๐‘ฆ โˆˆ โ„‹ โ†’ ( ๐‘ง โˆˆ ( span โ€˜ { ๐‘ฆ } ) โ†” โˆƒ ๐‘ค โˆˆ โ„‚ ๐‘ง = ( ๐‘ค ยทโ„Ž ๐‘ฆ ) ) )
61 60 adantr โŠข ( ( ๐‘ฆ โˆˆ โ„‹ โˆง ๐‘ง โˆˆ โ„‹ ) โ†’ ( ๐‘ง โˆˆ ( span โ€˜ { ๐‘ฆ } ) โ†” โˆƒ ๐‘ค โˆˆ โ„‚ ๐‘ง = ( ๐‘ค ยทโ„Ž ๐‘ฆ ) ) )
62 59 61 sylibrd โŠข ( ( ๐‘ฆ โˆˆ โ„‹ โˆง ๐‘ง โˆˆ โ„‹ ) โ†’ ( ( span โ€˜ { ( ๐‘ฆ +โ„Ž ๐‘ง ) } ) = ( span โ€˜ { ๐‘ฆ } ) โ†’ ๐‘ง โˆˆ ( span โ€˜ { ๐‘ฆ } ) ) )
63 62 adantr โŠข ( ( ( ๐‘ฆ โˆˆ โ„‹ โˆง ๐‘ง โˆˆ โ„‹ ) โˆง ๐‘ง โ‰  0โ„Ž ) โ†’ ( ( span โ€˜ { ( ๐‘ฆ +โ„Ž ๐‘ง ) } ) = ( span โ€˜ { ๐‘ฆ } ) โ†’ ๐‘ง โˆˆ ( span โ€˜ { ๐‘ฆ } ) ) )
64 spansneleq โŠข ( ( ๐‘ฆ โˆˆ โ„‹ โˆง ๐‘ง โ‰  0โ„Ž ) โ†’ ( ๐‘ง โˆˆ ( span โ€˜ { ๐‘ฆ } ) โ†’ ( span โ€˜ { ๐‘ง } ) = ( span โ€˜ { ๐‘ฆ } ) ) )
65 eqcom โŠข ( ( span โ€˜ { ๐‘ง } ) = ( span โ€˜ { ๐‘ฆ } ) โ†” ( span โ€˜ { ๐‘ฆ } ) = ( span โ€˜ { ๐‘ง } ) )
66 64 65 syl6ib โŠข ( ( ๐‘ฆ โˆˆ โ„‹ โˆง ๐‘ง โ‰  0โ„Ž ) โ†’ ( ๐‘ง โˆˆ ( span โ€˜ { ๐‘ฆ } ) โ†’ ( span โ€˜ { ๐‘ฆ } ) = ( span โ€˜ { ๐‘ง } ) ) )
67 66 adantlr โŠข ( ( ( ๐‘ฆ โˆˆ โ„‹ โˆง ๐‘ง โˆˆ โ„‹ ) โˆง ๐‘ง โ‰  0โ„Ž ) โ†’ ( ๐‘ง โˆˆ ( span โ€˜ { ๐‘ฆ } ) โ†’ ( span โ€˜ { ๐‘ฆ } ) = ( span โ€˜ { ๐‘ง } ) ) )
68 63 67 syld โŠข ( ( ( ๐‘ฆ โˆˆ โ„‹ โˆง ๐‘ง โˆˆ โ„‹ ) โˆง ๐‘ง โ‰  0โ„Ž ) โ†’ ( ( span โ€˜ { ( ๐‘ฆ +โ„Ž ๐‘ง ) } ) = ( span โ€˜ { ๐‘ฆ } ) โ†’ ( span โ€˜ { ๐‘ฆ } ) = ( span โ€˜ { ๐‘ง } ) ) )
69 29 68 sylan9r โŠข ( ( ( ( ๐‘ฆ โˆˆ โ„‹ โˆง ๐‘ง โˆˆ โ„‹ ) โˆง ๐‘ง โ‰  0โ„Ž ) โˆง ๐ด = ( span โ€˜ { ๐‘ฆ } ) ) โ†’ ( ( span โ€˜ { ( ๐‘ฆ +โ„Ž ๐‘ง ) } ) = ๐ด โ†’ ( span โ€˜ { ๐‘ฆ } ) = ( span โ€˜ { ๐‘ง } ) ) )
70 69 necon3d โŠข ( ( ( ( ๐‘ฆ โˆˆ โ„‹ โˆง ๐‘ง โˆˆ โ„‹ ) โˆง ๐‘ง โ‰  0โ„Ž ) โˆง ๐ด = ( span โ€˜ { ๐‘ฆ } ) ) โ†’ ( ( span โ€˜ { ๐‘ฆ } ) โ‰  ( span โ€˜ { ๐‘ง } ) โ†’ ( span โ€˜ { ( ๐‘ฆ +โ„Ž ๐‘ง ) } ) โ‰  ๐ด ) )
71 70 adantlrl โŠข ( ( ( ( ๐‘ฆ โˆˆ โ„‹ โˆง ๐‘ง โˆˆ โ„‹ ) โˆง ( ๐‘ฆ โ‰  0โ„Ž โˆง ๐‘ง โ‰  0โ„Ž ) ) โˆง ๐ด = ( span โ€˜ { ๐‘ฆ } ) ) โ†’ ( ( span โ€˜ { ๐‘ฆ } ) โ‰  ( span โ€˜ { ๐‘ง } ) โ†’ ( span โ€˜ { ( ๐‘ฆ +โ„Ž ๐‘ง ) } ) โ‰  ๐ด ) )
72 71 adantrr โŠข ( ( ( ( ๐‘ฆ โˆˆ โ„‹ โˆง ๐‘ง โˆˆ โ„‹ ) โˆง ( ๐‘ฆ โ‰  0โ„Ž โˆง ๐‘ง โ‰  0โ„Ž ) ) โˆง ( ๐ด = ( span โ€˜ { ๐‘ฆ } ) โˆง ๐ต = ( span โ€˜ { ๐‘ง } ) ) ) โ†’ ( ( span โ€˜ { ๐‘ฆ } ) โ‰  ( span โ€˜ { ๐‘ง } ) โ†’ ( span โ€˜ { ( ๐‘ฆ +โ„Ž ๐‘ง ) } ) โ‰  ๐ด ) )
73 72 imp โŠข ( ( ( ( ( ๐‘ฆ โˆˆ โ„‹ โˆง ๐‘ง โˆˆ โ„‹ ) โˆง ( ๐‘ฆ โ‰  0โ„Ž โˆง ๐‘ง โ‰  0โ„Ž ) ) โˆง ( ๐ด = ( span โ€˜ { ๐‘ฆ } ) โˆง ๐ต = ( span โ€˜ { ๐‘ง } ) ) ) โˆง ( span โ€˜ { ๐‘ฆ } ) โ‰  ( span โ€˜ { ๐‘ง } ) ) โ†’ ( span โ€˜ { ( ๐‘ฆ +โ„Ž ๐‘ง ) } ) โ‰  ๐ด )
74 eqeq2 โŠข ( ๐ต = ( span โ€˜ { ๐‘ง } ) โ†’ ( ( span โ€˜ { ( ๐‘ฆ +โ„Ž ๐‘ง ) } ) = ๐ต โ†” ( span โ€˜ { ( ๐‘ฆ +โ„Ž ๐‘ง ) } ) = ( span โ€˜ { ๐‘ง } ) ) )
75 74 biimpd โŠข ( ๐ต = ( span โ€˜ { ๐‘ง } ) โ†’ ( ( span โ€˜ { ( ๐‘ฆ +โ„Ž ๐‘ง ) } ) = ๐ต โ†’ ( span โ€˜ { ( ๐‘ฆ +โ„Ž ๐‘ง ) } ) = ( span โ€˜ { ๐‘ง } ) ) )
76 spansneleqi โŠข ( ( ๐‘ฆ +โ„Ž ๐‘ง ) โˆˆ โ„‹ โ†’ ( ( span โ€˜ { ( ๐‘ฆ +โ„Ž ๐‘ง ) } ) = ( span โ€˜ { ๐‘ง } ) โ†’ ( ๐‘ฆ +โ„Ž ๐‘ง ) โˆˆ ( span โ€˜ { ๐‘ง } ) ) )
77 9 76 syl โŠข ( ( ๐‘ฆ โˆˆ โ„‹ โˆง ๐‘ง โˆˆ โ„‹ ) โ†’ ( ( span โ€˜ { ( ๐‘ฆ +โ„Ž ๐‘ง ) } ) = ( span โ€˜ { ๐‘ง } ) โ†’ ( ๐‘ฆ +โ„Ž ๐‘ง ) โˆˆ ( span โ€˜ { ๐‘ง } ) ) )
78 elspansn โŠข ( ๐‘ง โˆˆ โ„‹ โ†’ ( ( ๐‘ฆ +โ„Ž ๐‘ง ) โˆˆ ( span โ€˜ { ๐‘ง } ) โ†” โˆƒ ๐‘ฃ โˆˆ โ„‚ ( ๐‘ฆ +โ„Ž ๐‘ง ) = ( ๐‘ฃ ยทโ„Ž ๐‘ง ) ) )
79 78 adantl โŠข ( ( ๐‘ฆ โˆˆ โ„‹ โˆง ๐‘ง โˆˆ โ„‹ ) โ†’ ( ( ๐‘ฆ +โ„Ž ๐‘ง ) โˆˆ ( span โ€˜ { ๐‘ง } ) โ†” โˆƒ ๐‘ฃ โˆˆ โ„‚ ( ๐‘ฆ +โ„Ž ๐‘ง ) = ( ๐‘ฃ ยทโ„Ž ๐‘ง ) ) )
80 35 ad2antlr โŠข ( ( ( ( ๐‘ฆ โˆˆ โ„‹ โˆง ๐‘ง โˆˆ โ„‹ ) โˆง ๐‘ฃ โˆˆ โ„‚ ) โˆง ( ๐‘ฆ +โ„Ž ๐‘ง ) = ( ๐‘ฃ ยทโ„Ž ๐‘ง ) ) โ†’ ( ๐‘ฃ + - 1 ) โˆˆ โ„‚ )
81 hvmulcl โŠข ( ( ๐‘ฃ โˆˆ โ„‚ โˆง ๐‘ง โˆˆ โ„‹ ) โ†’ ( ๐‘ฃ ยทโ„Ž ๐‘ง ) โˆˆ โ„‹ )
82 81 ancoms โŠข ( ( ๐‘ง โˆˆ โ„‹ โˆง ๐‘ฃ โˆˆ โ„‚ ) โ†’ ( ๐‘ฃ ยทโ„Ž ๐‘ง ) โˆˆ โ„‹ )
83 82 adantll โŠข ( ( ( ๐‘ฆ โˆˆ โ„‹ โˆง ๐‘ง โˆˆ โ„‹ ) โˆง ๐‘ฃ โˆˆ โ„‚ ) โ†’ ( ๐‘ฃ ยทโ„Ž ๐‘ง ) โˆˆ โ„‹ )
84 hvsubadd โŠข ( ( ( ๐‘ฃ ยทโ„Ž ๐‘ง ) โˆˆ โ„‹ โˆง ๐‘ง โˆˆ โ„‹ โˆง ๐‘ฆ โˆˆ โ„‹ ) โ†’ ( ( ( ๐‘ฃ ยทโ„Ž ๐‘ง ) โˆ’โ„Ž ๐‘ง ) = ๐‘ฆ โ†” ( ๐‘ง +โ„Ž ๐‘ฆ ) = ( ๐‘ฃ ยทโ„Ž ๐‘ง ) ) )
85 83 41 40 84 syl3anc โŠข ( ( ( ๐‘ฆ โˆˆ โ„‹ โˆง ๐‘ง โˆˆ โ„‹ ) โˆง ๐‘ฃ โˆˆ โ„‚ ) โ†’ ( ( ( ๐‘ฃ ยทโ„Ž ๐‘ง ) โˆ’โ„Ž ๐‘ง ) = ๐‘ฆ โ†” ( ๐‘ง +โ„Ž ๐‘ฆ ) = ( ๐‘ฃ ยทโ„Ž ๐‘ง ) ) )
86 ax-hvcom โŠข ( ( ๐‘ฆ โˆˆ โ„‹ โˆง ๐‘ง โˆˆ โ„‹ ) โ†’ ( ๐‘ฆ +โ„Ž ๐‘ง ) = ( ๐‘ง +โ„Ž ๐‘ฆ ) )
87 86 adantr โŠข ( ( ( ๐‘ฆ โˆˆ โ„‹ โˆง ๐‘ง โˆˆ โ„‹ ) โˆง ๐‘ฃ โˆˆ โ„‚ ) โ†’ ( ๐‘ฆ +โ„Ž ๐‘ง ) = ( ๐‘ง +โ„Ž ๐‘ฆ ) )
88 87 eqeq1d โŠข ( ( ( ๐‘ฆ โˆˆ โ„‹ โˆง ๐‘ง โˆˆ โ„‹ ) โˆง ๐‘ฃ โˆˆ โ„‚ ) โ†’ ( ( ๐‘ฆ +โ„Ž ๐‘ง ) = ( ๐‘ฃ ยทโ„Ž ๐‘ง ) โ†” ( ๐‘ง +โ„Ž ๐‘ฆ ) = ( ๐‘ฃ ยทโ„Ž ๐‘ง ) ) )
89 85 88 bitr4d โŠข ( ( ( ๐‘ฆ โˆˆ โ„‹ โˆง ๐‘ง โˆˆ โ„‹ ) โˆง ๐‘ฃ โˆˆ โ„‚ ) โ†’ ( ( ( ๐‘ฃ ยทโ„Ž ๐‘ง ) โˆ’โ„Ž ๐‘ง ) = ๐‘ฆ โ†” ( ๐‘ฆ +โ„Ž ๐‘ง ) = ( ๐‘ฃ ยทโ„Ž ๐‘ง ) ) )
90 89 biimpar โŠข ( ( ( ( ๐‘ฆ โˆˆ โ„‹ โˆง ๐‘ง โˆˆ โ„‹ ) โˆง ๐‘ฃ โˆˆ โ„‚ ) โˆง ( ๐‘ฆ +โ„Ž ๐‘ง ) = ( ๐‘ฃ ยทโ„Ž ๐‘ง ) ) โ†’ ( ( ๐‘ฃ ยทโ„Ž ๐‘ง ) โˆ’โ„Ž ๐‘ง ) = ๐‘ฆ )
91 hvsubval โŠข ( ( ( ๐‘ฃ ยทโ„Ž ๐‘ง ) โˆˆ โ„‹ โˆง ๐‘ง โˆˆ โ„‹ ) โ†’ ( ( ๐‘ฃ ยทโ„Ž ๐‘ง ) โˆ’โ„Ž ๐‘ง ) = ( ( ๐‘ฃ ยทโ„Ž ๐‘ง ) +โ„Ž ( - 1 ยทโ„Ž ๐‘ง ) ) )
92 81 91 sylancom โŠข ( ( ๐‘ฃ โˆˆ โ„‚ โˆง ๐‘ง โˆˆ โ„‹ ) โ†’ ( ( ๐‘ฃ ยทโ„Ž ๐‘ง ) โˆ’โ„Ž ๐‘ง ) = ( ( ๐‘ฃ ยทโ„Ž ๐‘ง ) +โ„Ž ( - 1 ยทโ„Ž ๐‘ง ) ) )
93 ax-hvdistr2 โŠข ( ( ๐‘ฃ โˆˆ โ„‚ โˆง - 1 โˆˆ โ„‚ โˆง ๐‘ง โˆˆ โ„‹ ) โ†’ ( ( ๐‘ฃ + - 1 ) ยทโ„Ž ๐‘ง ) = ( ( ๐‘ฃ ยทโ„Ž ๐‘ง ) +โ„Ž ( - 1 ยทโ„Ž ๐‘ง ) ) )
94 14 93 mp3an2 โŠข ( ( ๐‘ฃ โˆˆ โ„‚ โˆง ๐‘ง โˆˆ โ„‹ ) โ†’ ( ( ๐‘ฃ + - 1 ) ยทโ„Ž ๐‘ง ) = ( ( ๐‘ฃ ยทโ„Ž ๐‘ง ) +โ„Ž ( - 1 ยทโ„Ž ๐‘ง ) ) )
95 92 94 eqtr4d โŠข ( ( ๐‘ฃ โˆˆ โ„‚ โˆง ๐‘ง โˆˆ โ„‹ ) โ†’ ( ( ๐‘ฃ ยทโ„Ž ๐‘ง ) โˆ’โ„Ž ๐‘ง ) = ( ( ๐‘ฃ + - 1 ) ยทโ„Ž ๐‘ง ) )
96 95 ancoms โŠข ( ( ๐‘ง โˆˆ โ„‹ โˆง ๐‘ฃ โˆˆ โ„‚ ) โ†’ ( ( ๐‘ฃ ยทโ„Ž ๐‘ง ) โˆ’โ„Ž ๐‘ง ) = ( ( ๐‘ฃ + - 1 ) ยทโ„Ž ๐‘ง ) )
97 96 adantll โŠข ( ( ( ๐‘ฆ โˆˆ โ„‹ โˆง ๐‘ง โˆˆ โ„‹ ) โˆง ๐‘ฃ โˆˆ โ„‚ ) โ†’ ( ( ๐‘ฃ ยทโ„Ž ๐‘ง ) โˆ’โ„Ž ๐‘ง ) = ( ( ๐‘ฃ + - 1 ) ยทโ„Ž ๐‘ง ) )
98 97 adantr โŠข ( ( ( ( ๐‘ฆ โˆˆ โ„‹ โˆง ๐‘ง โˆˆ โ„‹ ) โˆง ๐‘ฃ โˆˆ โ„‚ ) โˆง ( ๐‘ฆ +โ„Ž ๐‘ง ) = ( ๐‘ฃ ยทโ„Ž ๐‘ง ) ) โ†’ ( ( ๐‘ฃ ยทโ„Ž ๐‘ง ) โˆ’โ„Ž ๐‘ง ) = ( ( ๐‘ฃ + - 1 ) ยทโ„Ž ๐‘ง ) )
99 90 98 eqtr3d โŠข ( ( ( ( ๐‘ฆ โˆˆ โ„‹ โˆง ๐‘ง โˆˆ โ„‹ ) โˆง ๐‘ฃ โˆˆ โ„‚ ) โˆง ( ๐‘ฆ +โ„Ž ๐‘ง ) = ( ๐‘ฃ ยทโ„Ž ๐‘ง ) ) โ†’ ๐‘ฆ = ( ( ๐‘ฃ + - 1 ) ยทโ„Ž ๐‘ง ) )
100 oveq1 โŠข ( ๐‘ค = ( ๐‘ฃ + - 1 ) โ†’ ( ๐‘ค ยทโ„Ž ๐‘ง ) = ( ( ๐‘ฃ + - 1 ) ยทโ„Ž ๐‘ง ) )
101 100 rspceeqv โŠข ( ( ( ๐‘ฃ + - 1 ) โˆˆ โ„‚ โˆง ๐‘ฆ = ( ( ๐‘ฃ + - 1 ) ยทโ„Ž ๐‘ง ) ) โ†’ โˆƒ ๐‘ค โˆˆ โ„‚ ๐‘ฆ = ( ๐‘ค ยทโ„Ž ๐‘ง ) )
102 80 99 101 syl2anc โŠข ( ( ( ( ๐‘ฆ โˆˆ โ„‹ โˆง ๐‘ง โˆˆ โ„‹ ) โˆง ๐‘ฃ โˆˆ โ„‚ ) โˆง ( ๐‘ฆ +โ„Ž ๐‘ง ) = ( ๐‘ฃ ยทโ„Ž ๐‘ง ) ) โ†’ โˆƒ ๐‘ค โˆˆ โ„‚ ๐‘ฆ = ( ๐‘ค ยทโ„Ž ๐‘ง ) )
103 102 rexlimdva2 โŠข ( ( ๐‘ฆ โˆˆ โ„‹ โˆง ๐‘ง โˆˆ โ„‹ ) โ†’ ( โˆƒ ๐‘ฃ โˆˆ โ„‚ ( ๐‘ฆ +โ„Ž ๐‘ง ) = ( ๐‘ฃ ยทโ„Ž ๐‘ง ) โ†’ โˆƒ ๐‘ค โˆˆ โ„‚ ๐‘ฆ = ( ๐‘ค ยทโ„Ž ๐‘ง ) ) )
104 79 103 sylbid โŠข ( ( ๐‘ฆ โˆˆ โ„‹ โˆง ๐‘ง โˆˆ โ„‹ ) โ†’ ( ( ๐‘ฆ +โ„Ž ๐‘ง ) โˆˆ ( span โ€˜ { ๐‘ง } ) โ†’ โˆƒ ๐‘ค โˆˆ โ„‚ ๐‘ฆ = ( ๐‘ค ยทโ„Ž ๐‘ง ) ) )
105 77 104 syld โŠข ( ( ๐‘ฆ โˆˆ โ„‹ โˆง ๐‘ง โˆˆ โ„‹ ) โ†’ ( ( span โ€˜ { ( ๐‘ฆ +โ„Ž ๐‘ง ) } ) = ( span โ€˜ { ๐‘ง } ) โ†’ โˆƒ ๐‘ค โˆˆ โ„‚ ๐‘ฆ = ( ๐‘ค ยทโ„Ž ๐‘ง ) ) )
106 elspansn โŠข ( ๐‘ง โˆˆ โ„‹ โ†’ ( ๐‘ฆ โˆˆ ( span โ€˜ { ๐‘ง } ) โ†” โˆƒ ๐‘ค โˆˆ โ„‚ ๐‘ฆ = ( ๐‘ค ยทโ„Ž ๐‘ง ) ) )
107 106 adantl โŠข ( ( ๐‘ฆ โˆˆ โ„‹ โˆง ๐‘ง โˆˆ โ„‹ ) โ†’ ( ๐‘ฆ โˆˆ ( span โ€˜ { ๐‘ง } ) โ†” โˆƒ ๐‘ค โˆˆ โ„‚ ๐‘ฆ = ( ๐‘ค ยทโ„Ž ๐‘ง ) ) )
108 105 107 sylibrd โŠข ( ( ๐‘ฆ โˆˆ โ„‹ โˆง ๐‘ง โˆˆ โ„‹ ) โ†’ ( ( span โ€˜ { ( ๐‘ฆ +โ„Ž ๐‘ง ) } ) = ( span โ€˜ { ๐‘ง } ) โ†’ ๐‘ฆ โˆˆ ( span โ€˜ { ๐‘ง } ) ) )
109 108 adantr โŠข ( ( ( ๐‘ฆ โˆˆ โ„‹ โˆง ๐‘ง โˆˆ โ„‹ ) โˆง ๐‘ฆ โ‰  0โ„Ž ) โ†’ ( ( span โ€˜ { ( ๐‘ฆ +โ„Ž ๐‘ง ) } ) = ( span โ€˜ { ๐‘ง } ) โ†’ ๐‘ฆ โˆˆ ( span โ€˜ { ๐‘ง } ) ) )
110 spansneleq โŠข ( ( ๐‘ง โˆˆ โ„‹ โˆง ๐‘ฆ โ‰  0โ„Ž ) โ†’ ( ๐‘ฆ โˆˆ ( span โ€˜ { ๐‘ง } ) โ†’ ( span โ€˜ { ๐‘ฆ } ) = ( span โ€˜ { ๐‘ง } ) ) )
111 110 adantll โŠข ( ( ( ๐‘ฆ โˆˆ โ„‹ โˆง ๐‘ง โˆˆ โ„‹ ) โˆง ๐‘ฆ โ‰  0โ„Ž ) โ†’ ( ๐‘ฆ โˆˆ ( span โ€˜ { ๐‘ง } ) โ†’ ( span โ€˜ { ๐‘ฆ } ) = ( span โ€˜ { ๐‘ง } ) ) )
112 109 111 syld โŠข ( ( ( ๐‘ฆ โˆˆ โ„‹ โˆง ๐‘ง โˆˆ โ„‹ ) โˆง ๐‘ฆ โ‰  0โ„Ž ) โ†’ ( ( span โ€˜ { ( ๐‘ฆ +โ„Ž ๐‘ง ) } ) = ( span โ€˜ { ๐‘ง } ) โ†’ ( span โ€˜ { ๐‘ฆ } ) = ( span โ€˜ { ๐‘ง } ) ) )
113 75 112 sylan9r โŠข ( ( ( ( ๐‘ฆ โˆˆ โ„‹ โˆง ๐‘ง โˆˆ โ„‹ ) โˆง ๐‘ฆ โ‰  0โ„Ž ) โˆง ๐ต = ( span โ€˜ { ๐‘ง } ) ) โ†’ ( ( span โ€˜ { ( ๐‘ฆ +โ„Ž ๐‘ง ) } ) = ๐ต โ†’ ( span โ€˜ { ๐‘ฆ } ) = ( span โ€˜ { ๐‘ง } ) ) )
114 113 necon3d โŠข ( ( ( ( ๐‘ฆ โˆˆ โ„‹ โˆง ๐‘ง โˆˆ โ„‹ ) โˆง ๐‘ฆ โ‰  0โ„Ž ) โˆง ๐ต = ( span โ€˜ { ๐‘ง } ) ) โ†’ ( ( span โ€˜ { ๐‘ฆ } ) โ‰  ( span โ€˜ { ๐‘ง } ) โ†’ ( span โ€˜ { ( ๐‘ฆ +โ„Ž ๐‘ง ) } ) โ‰  ๐ต ) )
115 114 adantlrr โŠข ( ( ( ( ๐‘ฆ โˆˆ โ„‹ โˆง ๐‘ง โˆˆ โ„‹ ) โˆง ( ๐‘ฆ โ‰  0โ„Ž โˆง ๐‘ง โ‰  0โ„Ž ) ) โˆง ๐ต = ( span โ€˜ { ๐‘ง } ) ) โ†’ ( ( span โ€˜ { ๐‘ฆ } ) โ‰  ( span โ€˜ { ๐‘ง } ) โ†’ ( span โ€˜ { ( ๐‘ฆ +โ„Ž ๐‘ง ) } ) โ‰  ๐ต ) )
116 115 adantrl โŠข ( ( ( ( ๐‘ฆ โˆˆ โ„‹ โˆง ๐‘ง โˆˆ โ„‹ ) โˆง ( ๐‘ฆ โ‰  0โ„Ž โˆง ๐‘ง โ‰  0โ„Ž ) ) โˆง ( ๐ด = ( span โ€˜ { ๐‘ฆ } ) โˆง ๐ต = ( span โ€˜ { ๐‘ง } ) ) ) โ†’ ( ( span โ€˜ { ๐‘ฆ } ) โ‰  ( span โ€˜ { ๐‘ง } ) โ†’ ( span โ€˜ { ( ๐‘ฆ +โ„Ž ๐‘ง ) } ) โ‰  ๐ต ) )
117 116 imp โŠข ( ( ( ( ( ๐‘ฆ โˆˆ โ„‹ โˆง ๐‘ง โˆˆ โ„‹ ) โˆง ( ๐‘ฆ โ‰  0โ„Ž โˆง ๐‘ง โ‰  0โ„Ž ) ) โˆง ( ๐ด = ( span โ€˜ { ๐‘ฆ } ) โˆง ๐ต = ( span โ€˜ { ๐‘ง } ) ) ) โˆง ( span โ€˜ { ๐‘ฆ } ) โ‰  ( span โ€˜ { ๐‘ง } ) ) โ†’ ( span โ€˜ { ( ๐‘ฆ +โ„Ž ๐‘ง ) } ) โ‰  ๐ต )
118 spanpr โŠข ( ( ๐‘ฆ โˆˆ โ„‹ โˆง ๐‘ง โˆˆ โ„‹ ) โ†’ ( span โ€˜ { ( ๐‘ฆ +โ„Ž ๐‘ง ) } ) โŠ† ( span โ€˜ { ๐‘ฆ , ๐‘ง } ) )
119 118 adantr โŠข ( ( ( ๐‘ฆ โˆˆ โ„‹ โˆง ๐‘ง โˆˆ โ„‹ ) โˆง ( ๐ด = ( span โ€˜ { ๐‘ฆ } ) โˆง ๐ต = ( span โ€˜ { ๐‘ง } ) ) ) โ†’ ( span โ€˜ { ( ๐‘ฆ +โ„Ž ๐‘ง ) } ) โŠ† ( span โ€˜ { ๐‘ฆ , ๐‘ง } ) )
120 oveq12 โŠข ( ( ๐ด = ( span โ€˜ { ๐‘ฆ } ) โˆง ๐ต = ( span โ€˜ { ๐‘ง } ) ) โ†’ ( ๐ด โˆจโ„‹ ๐ต ) = ( ( span โ€˜ { ๐‘ฆ } ) โˆจโ„‹ ( span โ€˜ { ๐‘ง } ) ) )
121 df-pr โŠข { ๐‘ฆ , ๐‘ง } = ( { ๐‘ฆ } โˆช { ๐‘ง } )
122 121 fveq2i โŠข ( span โ€˜ { ๐‘ฆ , ๐‘ง } ) = ( span โ€˜ ( { ๐‘ฆ } โˆช { ๐‘ง } ) )
123 snssi โŠข ( ๐‘ฆ โˆˆ โ„‹ โ†’ { ๐‘ฆ } โŠ† โ„‹ )
124 snssi โŠข ( ๐‘ง โˆˆ โ„‹ โ†’ { ๐‘ง } โŠ† โ„‹ )
125 spanun โŠข ( ( { ๐‘ฆ } โŠ† โ„‹ โˆง { ๐‘ง } โŠ† โ„‹ ) โ†’ ( span โ€˜ ( { ๐‘ฆ } โˆช { ๐‘ง } ) ) = ( ( span โ€˜ { ๐‘ฆ } ) +โ„‹ ( span โ€˜ { ๐‘ง } ) ) )
126 123 124 125 syl2an โŠข ( ( ๐‘ฆ โˆˆ โ„‹ โˆง ๐‘ง โˆˆ โ„‹ ) โ†’ ( span โ€˜ ( { ๐‘ฆ } โˆช { ๐‘ง } ) ) = ( ( span โ€˜ { ๐‘ฆ } ) +โ„‹ ( span โ€˜ { ๐‘ง } ) ) )
127 122 126 eqtrid โŠข ( ( ๐‘ฆ โˆˆ โ„‹ โˆง ๐‘ง โˆˆ โ„‹ ) โ†’ ( span โ€˜ { ๐‘ฆ , ๐‘ง } ) = ( ( span โ€˜ { ๐‘ฆ } ) +โ„‹ ( span โ€˜ { ๐‘ง } ) ) )
128 spansnch โŠข ( ๐‘ฆ โˆˆ โ„‹ โ†’ ( span โ€˜ { ๐‘ฆ } ) โˆˆ Cโ„‹ )
129 spansnj โŠข ( ( ( span โ€˜ { ๐‘ฆ } ) โˆˆ Cโ„‹ โˆง ๐‘ง โˆˆ โ„‹ ) โ†’ ( ( span โ€˜ { ๐‘ฆ } ) +โ„‹ ( span โ€˜ { ๐‘ง } ) ) = ( ( span โ€˜ { ๐‘ฆ } ) โˆจโ„‹ ( span โ€˜ { ๐‘ง } ) ) )
130 128 129 sylan โŠข ( ( ๐‘ฆ โˆˆ โ„‹ โˆง ๐‘ง โˆˆ โ„‹ ) โ†’ ( ( span โ€˜ { ๐‘ฆ } ) +โ„‹ ( span โ€˜ { ๐‘ง } ) ) = ( ( span โ€˜ { ๐‘ฆ } ) โˆจโ„‹ ( span โ€˜ { ๐‘ง } ) ) )
131 127 130 eqtr2d โŠข ( ( ๐‘ฆ โˆˆ โ„‹ โˆง ๐‘ง โˆˆ โ„‹ ) โ†’ ( ( span โ€˜ { ๐‘ฆ } ) โˆจโ„‹ ( span โ€˜ { ๐‘ง } ) ) = ( span โ€˜ { ๐‘ฆ , ๐‘ง } ) )
132 120 131 sylan9eqr โŠข ( ( ( ๐‘ฆ โˆˆ โ„‹ โˆง ๐‘ง โˆˆ โ„‹ ) โˆง ( ๐ด = ( span โ€˜ { ๐‘ฆ } ) โˆง ๐ต = ( span โ€˜ { ๐‘ง } ) ) ) โ†’ ( ๐ด โˆจโ„‹ ๐ต ) = ( span โ€˜ { ๐‘ฆ , ๐‘ง } ) )
133 119 132 sseqtrrd โŠข ( ( ( ๐‘ฆ โˆˆ โ„‹ โˆง ๐‘ง โˆˆ โ„‹ ) โˆง ( ๐ด = ( span โ€˜ { ๐‘ฆ } ) โˆง ๐ต = ( span โ€˜ { ๐‘ง } ) ) ) โ†’ ( span โ€˜ { ( ๐‘ฆ +โ„Ž ๐‘ง ) } ) โŠ† ( ๐ด โˆจโ„‹ ๐ต ) )
134 133 adantlr โŠข ( ( ( ( ๐‘ฆ โˆˆ โ„‹ โˆง ๐‘ง โˆˆ โ„‹ ) โˆง ( ๐‘ฆ โ‰  0โ„Ž โˆง ๐‘ง โ‰  0โ„Ž ) ) โˆง ( ๐ด = ( span โ€˜ { ๐‘ฆ } ) โˆง ๐ต = ( span โ€˜ { ๐‘ง } ) ) ) โ†’ ( span โ€˜ { ( ๐‘ฆ +โ„Ž ๐‘ง ) } ) โŠ† ( ๐ด โˆจโ„‹ ๐ต ) )
135 134 adantr โŠข ( ( ( ( ( ๐‘ฆ โˆˆ โ„‹ โˆง ๐‘ง โˆˆ โ„‹ ) โˆง ( ๐‘ฆ โ‰  0โ„Ž โˆง ๐‘ง โ‰  0โ„Ž ) ) โˆง ( ๐ด = ( span โ€˜ { ๐‘ฆ } ) โˆง ๐ต = ( span โ€˜ { ๐‘ง } ) ) ) โˆง ( span โ€˜ { ๐‘ฆ } ) โ‰  ( span โ€˜ { ๐‘ง } ) ) โ†’ ( span โ€˜ { ( ๐‘ฆ +โ„Ž ๐‘ง ) } ) โŠ† ( ๐ด โˆจโ„‹ ๐ต ) )
136 neeq1 โŠข ( ๐‘ฅ = ( span โ€˜ { ( ๐‘ฆ +โ„Ž ๐‘ง ) } ) โ†’ ( ๐‘ฅ โ‰  ๐ด โ†” ( span โ€˜ { ( ๐‘ฆ +โ„Ž ๐‘ง ) } ) โ‰  ๐ด ) )
137 neeq1 โŠข ( ๐‘ฅ = ( span โ€˜ { ( ๐‘ฆ +โ„Ž ๐‘ง ) } ) โ†’ ( ๐‘ฅ โ‰  ๐ต โ†” ( span โ€˜ { ( ๐‘ฆ +โ„Ž ๐‘ง ) } ) โ‰  ๐ต ) )
138 sseq1 โŠข ( ๐‘ฅ = ( span โ€˜ { ( ๐‘ฆ +โ„Ž ๐‘ง ) } ) โ†’ ( ๐‘ฅ โŠ† ( ๐ด โˆจโ„‹ ๐ต ) โ†” ( span โ€˜ { ( ๐‘ฆ +โ„Ž ๐‘ง ) } ) โŠ† ( ๐ด โˆจโ„‹ ๐ต ) ) )
139 136 137 138 3anbi123d โŠข ( ๐‘ฅ = ( span โ€˜ { ( ๐‘ฆ +โ„Ž ๐‘ง ) } ) โ†’ ( ( ๐‘ฅ โ‰  ๐ด โˆง ๐‘ฅ โ‰  ๐ต โˆง ๐‘ฅ โŠ† ( ๐ด โˆจโ„‹ ๐ต ) ) โ†” ( ( span โ€˜ { ( ๐‘ฆ +โ„Ž ๐‘ง ) } ) โ‰  ๐ด โˆง ( span โ€˜ { ( ๐‘ฆ +โ„Ž ๐‘ง ) } ) โ‰  ๐ต โˆง ( span โ€˜ { ( ๐‘ฆ +โ„Ž ๐‘ง ) } ) โŠ† ( ๐ด โˆจโ„‹ ๐ต ) ) ) )
140 139 rspcev โŠข ( ( ( span โ€˜ { ( ๐‘ฆ +โ„Ž ๐‘ง ) } ) โˆˆ HAtoms โˆง ( ( span โ€˜ { ( ๐‘ฆ +โ„Ž ๐‘ง ) } ) โ‰  ๐ด โˆง ( span โ€˜ { ( ๐‘ฆ +โ„Ž ๐‘ง ) } ) โ‰  ๐ต โˆง ( span โ€˜ { ( ๐‘ฆ +โ„Ž ๐‘ง ) } ) โŠ† ( ๐ด โˆจโ„‹ ๐ต ) ) ) โ†’ โˆƒ ๐‘ฅ โˆˆ HAtoms ( ๐‘ฅ โ‰  ๐ด โˆง ๐‘ฅ โ‰  ๐ต โˆง ๐‘ฅ โŠ† ( ๐ด โˆจโ„‹ ๐ต ) ) )
141 27 73 117 135 140 syl13anc โŠข ( ( ( ( ( ๐‘ฆ โˆˆ โ„‹ โˆง ๐‘ง โˆˆ โ„‹ ) โˆง ( ๐‘ฆ โ‰  0โ„Ž โˆง ๐‘ง โ‰  0โ„Ž ) ) โˆง ( ๐ด = ( span โ€˜ { ๐‘ฆ } ) โˆง ๐ต = ( span โ€˜ { ๐‘ง } ) ) ) โˆง ( span โ€˜ { ๐‘ฆ } ) โ‰  ( span โ€˜ { ๐‘ง } ) ) โ†’ โˆƒ ๐‘ฅ โˆˆ HAtoms ( ๐‘ฅ โ‰  ๐ด โˆง ๐‘ฅ โ‰  ๐ต โˆง ๐‘ฅ โŠ† ( ๐ด โˆจโ„‹ ๐ต ) ) )
142 141 ex โŠข ( ( ( ( ๐‘ฆ โˆˆ โ„‹ โˆง ๐‘ง โˆˆ โ„‹ ) โˆง ( ๐‘ฆ โ‰  0โ„Ž โˆง ๐‘ง โ‰  0โ„Ž ) ) โˆง ( ๐ด = ( span โ€˜ { ๐‘ฆ } ) โˆง ๐ต = ( span โ€˜ { ๐‘ง } ) ) ) โ†’ ( ( span โ€˜ { ๐‘ฆ } ) โ‰  ( span โ€˜ { ๐‘ง } ) โ†’ โˆƒ ๐‘ฅ โˆˆ HAtoms ( ๐‘ฅ โ‰  ๐ด โˆง ๐‘ฅ โ‰  ๐ต โˆง ๐‘ฅ โŠ† ( ๐ด โˆจโ„‹ ๐ต ) ) ) )
143 8 142 sylbid โŠข ( ( ( ( ๐‘ฆ โˆˆ โ„‹ โˆง ๐‘ง โˆˆ โ„‹ ) โˆง ( ๐‘ฆ โ‰  0โ„Ž โˆง ๐‘ง โ‰  0โ„Ž ) ) โˆง ( ๐ด = ( span โ€˜ { ๐‘ฆ } ) โˆง ๐ต = ( span โ€˜ { ๐‘ง } ) ) ) โ†’ ( ๐ด โ‰  ๐ต โ†’ โˆƒ ๐‘ฅ โˆˆ HAtoms ( ๐‘ฅ โ‰  ๐ด โˆง ๐‘ฅ โ‰  ๐ต โˆง ๐‘ฅ โŠ† ( ๐ด โˆจโ„‹ ๐ต ) ) ) )
144 143 expl โŠข ( ( ๐‘ฆ โˆˆ โ„‹ โˆง ๐‘ง โˆˆ โ„‹ ) โ†’ ( ( ( ๐‘ฆ โ‰  0โ„Ž โˆง ๐‘ง โ‰  0โ„Ž ) โˆง ( ๐ด = ( span โ€˜ { ๐‘ฆ } ) โˆง ๐ต = ( span โ€˜ { ๐‘ง } ) ) ) โ†’ ( ๐ด โ‰  ๐ต โ†’ โˆƒ ๐‘ฅ โˆˆ HAtoms ( ๐‘ฅ โ‰  ๐ด โˆง ๐‘ฅ โ‰  ๐ต โˆง ๐‘ฅ โŠ† ( ๐ด โˆจโ„‹ ๐ต ) ) ) ) )
145 4 144 syl5bi โŠข ( ( ๐‘ฆ โˆˆ โ„‹ โˆง ๐‘ง โˆˆ โ„‹ ) โ†’ ( ( ( ๐‘ฆ โ‰  0โ„Ž โˆง ๐ด = ( span โ€˜ { ๐‘ฆ } ) ) โˆง ( ๐‘ง โ‰  0โ„Ž โˆง ๐ต = ( span โ€˜ { ๐‘ง } ) ) ) โ†’ ( ๐ด โ‰  ๐ต โ†’ โˆƒ ๐‘ฅ โˆˆ HAtoms ( ๐‘ฅ โ‰  ๐ด โˆง ๐‘ฅ โ‰  ๐ต โˆง ๐‘ฅ โŠ† ( ๐ด โˆจโ„‹ ๐ต ) ) ) ) )
146 145 rexlimivv โŠข ( โˆƒ ๐‘ฆ โˆˆ โ„‹ โˆƒ ๐‘ง โˆˆ โ„‹ ( ( ๐‘ฆ โ‰  0โ„Ž โˆง ๐ด = ( span โ€˜ { ๐‘ฆ } ) ) โˆง ( ๐‘ง โ‰  0โ„Ž โˆง ๐ต = ( span โ€˜ { ๐‘ง } ) ) ) โ†’ ( ๐ด โ‰  ๐ต โ†’ โˆƒ ๐‘ฅ โˆˆ HAtoms ( ๐‘ฅ โ‰  ๐ด โˆง ๐‘ฅ โ‰  ๐ต โˆง ๐‘ฅ โŠ† ( ๐ด โˆจโ„‹ ๐ต ) ) ) )
147 3 146 sylbir โŠข ( ( โˆƒ ๐‘ฆ โˆˆ โ„‹ ( ๐‘ฆ โ‰  0โ„Ž โˆง ๐ด = ( span โ€˜ { ๐‘ฆ } ) ) โˆง โˆƒ ๐‘ง โˆˆ โ„‹ ( ๐‘ง โ‰  0โ„Ž โˆง ๐ต = ( span โ€˜ { ๐‘ง } ) ) ) โ†’ ( ๐ด โ‰  ๐ต โ†’ โˆƒ ๐‘ฅ โˆˆ HAtoms ( ๐‘ฅ โ‰  ๐ด โˆง ๐‘ฅ โ‰  ๐ต โˆง ๐‘ฅ โŠ† ( ๐ด โˆจโ„‹ ๐ต ) ) ) )
148 1 2 147 syl2anb โŠข ( ( ๐ด โˆˆ HAtoms โˆง ๐ต โˆˆ HAtoms ) โ†’ ( ๐ด โ‰  ๐ต โ†’ โˆƒ ๐‘ฅ โˆˆ HAtoms ( ๐‘ฅ โ‰  ๐ด โˆง ๐‘ฅ โ‰  ๐ต โˆง ๐‘ฅ โŠ† ( ๐ด โˆจโ„‹ ๐ต ) ) ) )
149 148 3impia โŠข ( ( ๐ด โˆˆ HAtoms โˆง ๐ต โˆˆ HAtoms โˆง ๐ด โ‰  ๐ต ) โ†’ โˆƒ ๐‘ฅ โˆˆ HAtoms ( ๐‘ฅ โ‰  ๐ด โˆง ๐‘ฅ โ‰  ๐ต โˆง ๐‘ฅ โŠ† ( ๐ด โˆจโ„‹ ๐ต ) ) )